proposition: Lemma weaksum_r_opp_compat : forall (rAn' : Cv_radius_weak (- An) r), weaksum_r (- An)%Rseq r rAn' x = (- weaksum_r An r rAn)%F x.
proof: Proof. intros rAn'. assert (H1 := weaksum_r_sums (- An)%Rseq _ rAn' x x_bd) ; assert (H2 := Rpser_opp_compat _ _ _ (weaksum_r_sums An _ rAn x x_bd)) ; 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