proposition: Lemma power_series_conv : convergent (power_series c).
proof: Proof. intros. red in |- *. apply Cauchy_prop2_prop. cut ([1][-]c [#] [0]). intro H. exists ([1][/] _[//]H). apply power_series_Lim1. apply minus_ap_zero. apply Greater_imp_ap. eapply leEq_less_trans. apply leEq_AbsIR. assumption. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)