I am trying to solve the 1 star exercise in the ‘Logic’ chapter from ‘Logical Foundations’.

Theorem eqb_neq : ∀ x y : nat,

x =? y = false ↔ x ≠ y.

My attempt is to try to do this:

Proof.

intros x y. split.

- apply not_true_iff_false with (b := (x=?y)).

But I am not able to use the ‘apply’ tactic.

PS.

Lemma not_true_iff_false : forall b,

b <> true ↔ b = false.

Can someone help me out? Thanks!

Try

```
Theorem eqb_neq : ∀ x y : nat, x =? y = false ↔ x ≠ y.
Proof.
intros x y.
split.
- intros H.
apply not_true_iff_false in H.
```

Hi!

Thank you so much for your suggestion! I was able to complete the proof but it is not an elegant and short one. I introduce H1 and use eqb_refl. Is there an easier way that I’m overlooking?

I’m not sure how much you are allowed to assume. I mean the simplest proof is just

```
Theorem eqb_neq : ∀ x y : nat, x =? y = false ↔ x ≠ y.
Proof.
apply Nat.eqb_neq.
Qed.
```