proposition: Lemma T1limit_succ_tail : forall alpha n beta, nf beta -> ~ T1limit (cons alpha n (succ beta)).
proof: Proof. simpl;intros; destruct alpha. - discriminate. - case_eq (succ beta). + intro; now destruct (succ_not_zero beta). + intros gamma p delta H0; rewrite <- H0; now apply T1limit_succ. 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)