proposition: Lemma sum_plus_compat : forall (rAnBn : infinite_cv_radius (An + Bn)), sum (An + Bn)%Rseq rAnBn == (sum An rAn + sum Bn rBn)%F.
proof: Proof. intros rAnBn x. assert (Ha := sum_sums An rAn x) ; assert (Hb := sum_sums Bn rBn x) ; assert (H1 := sum_sums (An + Bn)%Rseq rAnBn x) ; assert (H2 := Rpser_add_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