proposition: Lemma Limit_not_Zero alpha : E0limit alpha -> alpha <> E0zero.
proof: Proof. destruct alpha; unfold E0limit, E0zero; cbn; intros H H0. injection H0; intro ; subst cnf0; eapply T1.T1limit_not_zero; eauto. 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)