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.

Answer 2

It's really easy (but the negation makes it a bit confusing).

Lemma not_eq_S2: forall m n, S m <> S n -> m <> n.
Proof.
  unfold not.      (*                             |- ... -> False *)
  intros m n H C.  (* ..., H : S m = S n -> False |- False *)
  apply H.         (* ...                         |- S m = S n *)
  (* f_equal gets rid of functions applied on both sides of an equality,
     this is probably what you didn't find *)
  (* basically, f_equal turns a goal [f a = f b] into [a = b] *)
  f_equal.         (* ..., C : m = n              |- m = n *)
  exact C.
Qed.