Does the standard library have a proof of "uniqueness of le proofs", i.e. ?
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:
Last updated: Oct 03 2023 at 20:01 UTC