logic - 如何在 Coq 中证明 (0 = 2) -> false？

Question

在一个引理的证明中，我最终达到了一个状态，其中

我有一个前提

H : 0 = 2

我必须证明

false.

问题：如何推断前提H是假的以得出证明？

标签： logiccoq

Answer 1

该discriminate策略可以处理这样的情况。我相信这easy也有效，就像 . 一样congruence，它比discriminate.