相关疑难解决方法(0)

假设我想证明以下定理:

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.

这个是微不足道的m,因为假设不能同时为后继和零.但是我发现证明这一点非常棘手,而且我不知道如何在没有辅助引理的情况下制作它:

Lemma succ_neq_zero_lemma : forall n : nat, O = S n -> False.
Proof.
  intros.
  inversion H.
Qed.

Theorem succ_neq_zero : forall n m: nat, S n = m -> 0 = m -> False.
Proof.
  intros.
  symmetry in H.
  apply (succ_neq_zero_lemma n).
  transitivity m.
  assumption.
  assumption.
Qed.

我很确定有更好的方法来证明这一点.最好的方法是什么？