證明 - 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。