proposition: Lemma sum_opp_compat : forall (rAn' : infinite_cv_radius (- An)), sum (- An)%Rseq rAn' == (- sum An rAn)%F.
proof: Proof. intros rAn' x. assert (H1 := sum_sums (- An)%Rseq rAn' x) ; assert (H2 := Rpser_opp_compat _ _ _ (sum_sums An rAn x)) ; eapply Rpser_unique ; eassumption. Qed.
imports: Reals Lra Rsequence Rseries_def Rseries_cv_facts Rpser_def Rpser_sums Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rinterval Rfunction_def Rextensionality