proposition: Lemma series_sum_minus : 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_minus. apply Lim_wd'. intro; simpl in |- *. unfold seq_part_sum in |- *. unfold cg_minus in |- *. eapply eq_transitive_unfolded. apply Sum0_plus_Sum0 with (g := fun n : nat => [--] (y n)). apply bin_op_wd_unfolded. algebra. apply inv_Sum0. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)