proposition: Lemma T1limit_cases : forall alpha n beta, nf (cons alpha n beta) -> T1limit (cons alpha n beta) -> { alpha <> zero /\ beta = zero} + {alpha <> zero /\ T1limit beta }.
proof: Proof. intros alpha n beta H; simpl; destruct alpha. - discriminate. - destruct beta. + left; split;auto. discriminate. + right; split; auto. * discriminate. Defined.
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)