If you have a denominator composed of “n - k - 1”, I hardly find it surprising that if n=3 and k=2 that you have a slight problem…
Anyway, check out Idris[2], it’s cool for this sort of thing
Anyway, check out Idris[2], it’s cool for this sort of thing
I would be more impressed when some mathematician finds a more severe error in their proofs with the help of theorem provers (meaning a mistake in their own intuition).