coqproofcoqide

Coq - How to prove eqb_neq?

I'm trying to prove eqb_neq:

Theorem eqb_neq : forall x y : nat,
  x =? y = false <-> x <> y.

This is my current proof status: enter image description here

During the proof I reached a final step where I just need to prove the additional helper theorem: 

Theorem eqb_false_helper : forall n m : nat,
    n <> m -> S n <> S m.

I've tried multiple strategies but now I'm not even sure it's possible to prove this helper theorem.

I'm not sure how to prove the base case using induction: enter image description here

What else can I try? Any tips for eqb_neq or the helper theorem?

Thanks

Solution

  • It is actually quite simple for your helper theorem if you just unfold not :

    Theorem eqb_false_helper : forall n m : nat,
    n <> m -> S n <> S m.
Proof.
unfold not; intros.
apply H; injection H0; intro; assumption.
Qed.

    You actually just need to prove that S n = S m -> False, you assume that n = m -> False, thus you can prove that S n = S m -> n = m, which is done injecting hypothesis S n = S m.