proposition: Lemma E0_lt_eq_lt alpha beta : alpha o< beta \/ alpha = beta \/ beta o< alpha.
proof: Proof. destruct (compare_correct alpha beta). - subst;right;now left. - now left. - right; now right. 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)