Does the standard library have a proof of "uniqueness of le proofs", i.e. $\forall n m (p_1 p_2 : n \le m), p_1 = p_2$?

Or some other library (without axioms)?

you mean le on natural numbers?

in mathcomp, the order is defined as a boolean relation, so you can use a generic axiom-free proof of uniqueness for such relations

IIANM also math-comp includes a proof for the standard library https://github.com/math-comp/math-comp/blob/2b97a257956d307e7cb9ad7d4920fb5db969b69b/mathcomp/ssreflect/ssrnat.v#L464

Note that the proof of this is very short, at least with Equations:

https://github.com/MetaCoq/metacoq/blob/abc736f20020156e520e7ca4ef0557ce5f8b7db0/pcuic/theories/PCUICWcbvEval.v#L693-L699

Last updated: Apr 14 2024 at 09:39 UTC