如何证明（0 <> 2）->在Coq中为假？

Question

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

我有一个前提

H : 0 = 2

并且我必须证明

false。

问题

：如何推断前提H为假以得出证明？

[证明一个引理后，我最终达到了一个前提，我的前提是H：0 = 2，我必须证明是错误的。问题：如何推断前提H为假以得出结论？

Answer 1

discriminate策略可以处理类似情况。我相信easy也可以，congruence也可以，它们比discriminate更通用。