proposition: Lemma c_exp_Lim : Cauchy_Lim_prop2 (power_series c) [0].
proof: Proof. red in |- *; intros eps H. elim (qi_yields_zero (AbsIR c) (AbsIR_nonneg _) Hc eps H). intros N Hn. exists N; intros. unfold power_series in |- *. astepr (c[^]m). apply AbsSmall_transitive with (c[^]N). apply AbsIR_imp_AbsSmall. eapply leEq_wdl. apply Hn. apply eq_symmetric_unfolded; apply (AbsIR_nexp c N). eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply (AbsIR_nexp c m). eapply leEq_wdr. 2: apply eq_symmetric_unfolded; apply (AbsIR_nexp c N). change ((AbsIR c)[^]m[<=](AbsIR c)[^]N). apply nexp_resp_le'. apply AbsIR_nonneg. apply less_leEq; assumption. assumption. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)