proposition: Lemma series_seq_Lim : convergent -> Cauchy_Lim_prop2 x [0].
proof: Proof. intros H. red in |- *. intros eps H0. red in H. red in H. elim (H _ (pos_div_two _ _ H0)). intros N HN. exists (Nat.max N 1); intros. apply AbsSmall_wdr_unfolded with (seq_part_sum (S m) [-]seq_part_sum m). apply AbsSmall_wdr_unfolded with (seq_part_sum (S m) [-]seq_part_sum N[+] (seq_part_sum N[-]seq_part_sum m)). rstepl (eps [/]TwoNZ[+]eps [/]TwoNZ). apply AbsSmall_plus. apply HN. apply Nat.le_trans with (Nat.max N 1); auto with arith. apply AbsSmall_minus; apply HN. apply Nat.le_trans with (Nat.max N 1); auto with arith. rational. eapply eq_transitive_unfolded. apply seq_part_sum_n; auto with arith. simpl in |- *; astepr (x m); apply Sum_one. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)