proposition: Lemma power_series_Lim1 : forall H : [1][-]c [#] [0], Cauchy_Lim_prop2 (seq_part_sum (power_series c)) ([1][/] _[//]H).
proof: Proof. intro. red in |- *. intros. unfold power_series in |- *; unfold seq_part_sum in |- *. cut ({N : nat | (AbsIR c)[^]N [<=] eps[*]AbsIR ([1][-]c)}). intro H1. elim H1; clear H1; intros N HN. exists N; intros. apply AbsSmall_wdr_unfolded with ( [--] (c[^]m[/] _[//]H)). apply inv_resp_AbsSmall. apply AbsIR_imp_AbsSmall. eapply leEq_wdl. 2: apply eq_symmetric_unfolded. 2: apply (AbsIR_division (c[^]m) ([1][-]c) H (AbsIR_resp_ap_zero _ H)). apply shift_div_leEq. apply AbsIR_pos; assumption. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply AbsIR_nexp_op. eapply leEq_transitive. 2: apply HN. apply nexp_resp_le'; auto. apply AbsIR_nonneg. apply less_leEq; auto. astepl ( [--] (c[^]m[/] _[//]H) [+] ([1][/] _[//]H) [-] ([1][/] _[//]H)). apply cg_minus_wd. 2: algebra. cut (c[-][1] [#] [0]). intros H2. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. apply Sum0_c_exp with (H := H2). rational. apply minus_ap_zero. apply ap_symmetric. apply zero_minus_apart. assumption. apply qi_yields_zero. apply AbsIR_nonneg. assumption. apply less_wdl with ([0][*]AbsIR ([1][-]c)). apply mult_resp_less. assumption. apply AbsIR_pos. assumption. apply cring_mult_zero_op. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)