proposition: Lemma E0_not_Lt_zero alpha : ~ alpha o< E0zero.
proof: Proof. destruct alpha; unfold E0lt; cbn. intros [H [H0 H1]]; eapply not_lt_zero; eauto. 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)