proposition: Lemma weaksum_r_minus_compat : forall (rAnBn : Cv_radius_weak (An - Bn) r), weaksum_r (An - Bn)%Rseq r rAnBn x = (weaksum_r An r rAn - weaksum_r Bn r rBn)%F x.
proof: Proof. intros rAnBn. assert (Ha := weaksum_r_sums An r rAn x x_bd) ; assert (Hb := weaksum_r_sums Bn r rBn x x_bd) ; assert (H1 := weaksum_r_sums (An - Bn)%Rseq r rAnBn x x_bd) ; assert (H2 := Rpser_minus_compat _ _ _ _ _ Ha Hb) ; 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