proposition: Lemma Succ_not_T1limit alpha : E0is_succ alpha -> ~ E0limit alpha .
proof: Proof. red; destruct alpha; unfold E0is_succ, E0limit; cbn. intros H H0. rewrite (succ_not_limit _ H) in H0. discriminate. 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)