证明 - X> = A/\ X <= a -> X = A

Question

一个人怎么会去证明以下

Theorem T: forall x, a: nat, x >= a /\ x <= a -> x = a. 

在勒柯克

？

Answer 1

如果你不想使用的omega全部力量，我将搜索标准库使用SearchPattern或SearchAbout（或谷歌）和apply le_antisym的<=反对称财产。

如果你想要一个没有使用引理库的证明，可以通过归纳于x和a。