proposition: Lemma le_canonical_nn {n} : le_canonical n n = left (le_n _).
proof: Proof. induction n; simpl; try reflexivity. rewrite IHn; clear IHn. edestruct le_canonical; [ exfalso | reflexivity ]. { eapply Nat.nle_succ_diag_l; eassumption. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Program.Basics