The Coq mailing list

[Jack Kolb <kolb0128 AT umn.edu>]

Hi,

I am still new to Coq, so bear with me if I'm missing something obvious.

I have encountered a problem with the induction tactic when trying to prove the following simple theorem:

    Theorem Sn_le_Sm__n_le_m : forall n m,

      S n <= S m -> n <= m.

My instinct is to start the proof like so:

    Proof.

      intros. induction H.

However, the induction tactic doesn't preserve any information about n and m, and I am unable to make any forward progress. It is possible that I'm overlooking something, but this seems to be a problem with the induction tactic. I've done some research and found a similar situation here: http://stackoverflow.com/questions/4519692/keeping-information-when-using-induction. However, the suggestions made in this post don't seem to solve my problem.

Is there some way to use induction while preserving the information about n and m?

Thanks.