proposition: Lemma series_sum_plus : forall H : convergent (fun n => x n[+]y n), series_sum _ H [=] series_sum _ convX[+]series_sum _ convY.
proof: Proof. intros. unfold series_sum in |- *. eapply eq_transitive_unfolded. 2: apply Lim_plus. apply Lim_wd'. intro; simpl in |- *. unfold seq_part_sum in |- *. apply Sum0_plus_Sum0. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)