proposition: Lemma le_lt_eq_dec : forall alpha beta, alpha o<= beta -> {alpha o< beta} + {alpha = beta}.
proof: Proof. destruct alpha, beta. intros. rewrite Le_iff in H. destruct (LE_LT_eq_dec H). - now left. - cbn in e; subst. right; subst; f_equal; apply nf_proof_unicity. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles ArithRing Wellfounded Operators_Properties Logic.Eqdep_dec) hydras(Prelude.More_Arith Prelude.Restriction Prelude.DecPreOrder ON_Generic OrdNotations)