proposition: Lemma series_sum_inv : forall H : convergent (fun n => [--] (x n)), series_sum _ H [=] [--] (series_sum _ convX).
proof: Proof. intros. set (y := Cauchy_const [0]) in *. cut (convergent y). intros H0. eapply eq_transitive_unfolded. apply series_sum_wd with (y := fun n : nat => y n[-]x n) (convY := conv_series_minus _ _ H0 convX). intro; unfold y in |- *; simpl in |- *; algebra. cut (series_sum y H0 [=] [0]); intros. astepr ([0][-]series_sum x convX). astepr (series_sum y H0[-]series_sum x convX). apply series_sum_minus. apply series_sum_zero. apply conv_zero_series. Qed.
imports: CoRN.reals.CSumsReals CoRN.reals.NRootIR Coq(Lia)