1

如何证明以下内容

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

在考克?

4

1 回答 1

0

如果您不想使用 的全部功能omega,我会在标准库中搜索<=使用SearchPatternor SearchAbout(或谷歌)和apply le_antisym.

如果您想在不使用库中的引理的情况下进行证明,请在xand上进行归纳a

于 2015-10-09T07:01:30.487 回答