proposition: Lemma pred_of_limitR : forall alpha, nf alpha -> alpha <> zero -> pred alpha = None -> T1limit alpha.
proof: Proof. intros alpha Halpha; destruct (zero_limit_succ_dec Halpha). - destruct s; auto. - destruct s as [x [H H0]]; subst. rewrite pred_of_succ; auto. + discriminate. Qed.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)