问证明x >= a /\ x <= a -> x=a
EN

Stack Overflow用户

提问于 2015-10-09 05:52:48

回答 1查看 57关注 0票数 1

如何证明以下几点：

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

在科克？

回答已采纳

发布于 2015-10-09 07:01:30

如果您不想使用omega的全部功能，我将使用SearchPattern或SearchAbout (或谷歌)和apply le_antisym在标准库中搜索<=的反对称属性。

如果您想要一个不使用库中的引理的证明，可以在x和a上进行归纳。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/33030819

复制

相似问题

问证明x >= a /\ x <= a -> x=aEN