如何证明Coq中的le_antisym定理？是否可借助le_trans？

已知已证定理 #

Theorem le_trans: forall n m o, n <= m -> m <= o -> n <= o.
Proof.
 intros n m o Lnm Lmo.
 generalize dependent Lnm.  
 generalize dependent n.
 induction Lmo.
 - intros. apply Lnm.
 - intros. apply le_S. apply IHLmo. apply Lnm.
Qed.

待证定理 #

Theorem le_antisym: forall n m, n <= m -> m <= n -> n = m.

命题关联与证明说明 #

• 命题关联：le_trans描述自然数上<=关系的传递性，le_antisym描述其反对称性，二者都是偏序关系的核心性质，但证明逻辑相互独立，le_antisym的证明不需要依赖le_trans。
• 是否需要le_trans：不需要直接借助le_trans，基于<=的归纳定义直接证明更简洁直观。

不借助le_trans的证明方案 #

直接对其中一个<=假设做归纳，结合le的定义与自然数的基础性质推导：

Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m.
Proof.
  intros n m Hnm Hmn.
  induction Hnm as [|m' Hnm IH].
  - (* 基础情况：Hnm是le_n，即n <= n，此时m必然等于n *)
    reflexivity.
  - (* 归纳情况：Hnm是le_S，即m = S m' 且 n <= m' *)
    inversion Hmn as [|n' Hmn'].
    + (* 子情况1：Hmn是le_n，即m <= m，结合m = S m'会与n <= m'产生矛盾，inversion自动消解该情况 *)
      inversion Hnm.
    + (* 子情况2：Hmn是le_S，即n = S n' 且 m <= n'，结合m = S m'可得m' <= n'，调用归纳假设完成证明 *)
      apply IH. apply Hmn'.
Qed.

硬借助le_trans的情况（不推荐） #

这种方法完全冗余，因为le_trans只能推出n <= n和m <= m这类自反性结论，无法直接建立n=m的等式，最终还是要回到le的归纳定义和自然数的基础性质上推导，绕远路且无意义。

内容的提问来源于stack exchange，提问作者sesame ball