Is there an equivalent of the uniqueness of identity proofs, for types with a decidable order ? In particular, in the type of Peano natural numbers ? Is it implemented somewhere in Coq's library ? (I couldn't find it)
It seems true on the natural numbers, because a proof that n <= p looks the same as a proof of n == p : it iteratively destructs n and p until the number on the left reaches 0, then concludes.
Mathcomp has a lemma like that, i.e.
Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat.
together with its proof in ssrnat.v. Notice the coq_nat scope, which means we are using the inductive definition of <=, as opposed to Mathcomp's boolean version mentioned by @ejgallego.
The way I see it is that the type of the decidable operators should not land in Prop but in bool, as done in Math-Comp.
This way, if <= : T -> T -> bool you get irrelevance pretty easily.