proposition: Lemma le_proof_irrelevance' {n m} (pf : {n <= m} + {~n <= m}) : le_canonical n m = match pf, le_canonical n m with | left pf', _ => left pf' | _, right pf' => right pf' | right pf', left pf'' => match pf' pf'' with end end.
proof: Proof. destruct pf. { erewrite <- le_proof_irrelevance_left; reflexivity. } { edestruct le_canonical; try reflexivity. exfalso; eauto. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Program.Basics