proposition: Lemma conv_zero_series : convergent (fun n => [0]).
proof: Proof. exists 0. intros. simpl in |- *. eapply AbsSmall_wdr_unfolded. apply zero_AbsSmall; apply less_leEq; assumption. unfold seq_part_sum in |- *. induction m as [| m Hrecm]. simpl in |- *; algebra. simpl in |- *. eapply eq_transitive_unfolded. apply Hrecm; auto with arith. rational. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)