How do I teach GHC that n < n + 1?

I wrote this, but it doesn't quite seem to work:

This doesn't work because 'm' and 'S m' aren't equal, but they're also not NOT equal, so Haskell never gets past the first clause of IsConstPlus:
https://twitter.com/fancytypes/status/1369834087226216448?s=20

@cyrridven yeah you're gonna wanna recurse all the way down to the base case

@lambdagrrl honestly, if Haskell allows me two write infinite types like 'S (S (S ...))' then why not infinite pattern matches?

@cyrridven wait where is the infinite match?

@lambdagrrl I've been wanting to actually try and construct one, 'cuz I think it should be possible if GHC can be persuaded not to unroll 'type family Inf where Inf = S Inf' too much.