如何从〜a <> b]证明a = b

Question

像标题一样，我无法弄清楚证明这种问题的策略，任何建议将不胜感激。ps。 a和b的类型均为nat * nat。

像标题一样，我无法弄清楚证明这种问题的策略，任何建议将不胜感激。 ps。 a和b的类型均为nat * nat。

Answer 1

您应使用not_not中的not_not：如果属性是可判定的，则可以基于其双重否定的证明为其构造证明。