proposition: Lemma le_proof_irrelevance {n m} (pf pf' : n <= m) : pf = pf'.
proof: Proof. transitivity (match le_canonical n m with | left pf' => pf' | right pf' => match pf' pf with end end). { rewrite (le_proof_irrelevance' (left pf)); reflexivity. } { rewrite (le_proof_irrelevance' (left pf')); reflexivity. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Program.Basics