Find centralized, trusted content and collaborate around the technologies you use most.
Teams
Q&A for work
Connect and share knowledge within a single location that is structured and easy to search.
如何证明以下内容
Theorem T: forall x, a: nat, x >= a /\ x <= a -> x = a.
在考克?
如果您不想使用 的全部功能omega,我会在标准库中搜索<=使用SearchPatternor SearchAbout(或谷歌)和apply le_antisym.
omega
<=
SearchPattern
SearchAbout
apply le_antisym
如果您想在不使用库中的引理的情况下进行证明,请在xand上进行归纳a。
x
a