I have natural number n as input argument in a function. Have pattern matching on it , It may be 0 or S n'. When I perform induction I get 0 & S n. S n is some greater number of n. But it should be S n'( any number not necessary greater).Why this happen?

S n is not a bigger number than the original n, because it uses an unrelated n.

the tactic "induction n" removes the original n from the context, and introduces an unrelated n.

Last updated: Jun 25 2024 at 18:02 UTC