proposition: Lemma E0_lt_ge alpha beta : alpha o< beta \/ beta o<= alpha.
proof: Proof. destruct (E0_lt_eq_lt alpha beta) as [H | [ | H]]. - now left. - subst; right. apply Le_refl. - right; now apply Lt_Le_incl. 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)