proposition: Lemma Succ_lt_T1limit alpha beta: E0limit alpha -> beta o< alpha -> E0_succ beta o< alpha.
proof: Proof. destruct alpha, beta;unfold E0lt; cbn. intros; apply succ_lt_limit; auto. 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)