对于具有可确定顺序的类型，是否存在等效于身份证明的唯一性？特别是，在 Peano 自然数的类型中？它是在 Coq 库的某个地方实现的吗？ (没找到)
这在自然数上似乎是正确的，因为证明 n <= p看起来与 n == p 的证明相同:它迭代地破坏n和 p直到左边的数字为0，结束。
最佳答案
Mathcomp 有一个类似的引理，即
Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat.
连同其在 ssrnat.v 中的证明。请注意 coq_nat 范围，这意味着我们正在使用 <= 的归纳定义，而不是@ejgallego 提到的 Mathcomp 的 bool 版本。
关于coq - 主要证明的唯一性，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/53888104/