Coq - 如何证明 eqb_neq？

Question

我想证明eqb_neq:

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

这是我目前的证明状态：

在证明过程中，我到达了最后一步，我只需要证明附加的辅助定理：

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

我已经尝试了多种策略，但现在我什至不确定是否有可能证明这个辅助定理。

我不确定如何使用归纳来证明基本情况：

我还能尝试什么？ eqb_neq 或辅助定理的任何提示？

谢谢

Answer 1

如果你不展开的话，你的辅助定理实际上很简单:

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.

你其实只需要证明S n = S m -> False，你假设n = m -> False，这样你就可以证明S n = S m -> n = m，这是通过注入假设S n = S m完成的。