proposition: Lemma series_sum_wd : (forall n, x n [=] y n) -> series_sum _ convX [=] series_sum _ convY.
proof: Proof. intros. unfold series_sum in |- *. apply Lim_wd'. intro; simpl in |- *. unfold seq_part_sum in |- *. apply Sum0_wd; assumption. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)