proposition: Lemma series_sum_zero : forall H : convergent (fun n => [0]), series_sum _ H [=] [0].
proof: Proof. intro. unfold series_sum in |- *. apply eq_symmetric_unfolded; apply Limits_unique. 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)