我可以在Coq

Question

lemma帮助：forall n nx：nat，0<= n - S nx ->n -s nx + 1 = n -nx。证明。 ....

我经常考虑过这一点，我已经归纳了，甚至问了LLM ...即使这是一个非常简单的引理，我也没有结果。感谢您提前的帮助。

Answer 1

n = nx = 0

（例如使用

destruct n

和

destruct nx

）并简化，则会得到

0 <= 0 -> 1 = 0

。

问题是引理简直是错误的。