Not equal succesors in Coq

Question

I am trying to prove the following lemma in Coq:

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.

It seems easy but I do not find how to finish the proof. Can anybody help me please?

Thank you.

Answer 1

The thing to know is that in Coq, a negation is a function that implies False, so the S m <> S n is really S m = S n -> False. So instead of proving n <> m we can introduce the n = m (we can either unfold not or tell intros explicitly to do it) and get the goal False instead. But with n = m in the context we can rewrite HS: S n <> S m into HS: S n <> S n, which can be handled by auto, or many other tactics such as apply HS. reflexivity. or congruence. etc.

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.

Proof. intros m n HS HC. 
  rewrite HC in HS. auto.
Qed.