proposition: Lemma E0_Lt_irrefl (alpha : E0) : ~ alpha o< alpha.
proof: Proof. destruct alpha;unfold E0lt;cbn;apply LT_irrefl. 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)