proposition: Lemma sum_r_mult_compat : forall (rAnBn : finite_cv_radius (An # Bn) r), sum_r (An # Bn)%Rseq r rAnBn x = (sum_r An r rAn * sum_r Bn r rBn)%F x.
proof: Proof. intros rAnBn. assert (rAn' : Cv_radius_weak An (middle (Rabs x) r)). apply rAn ; split ; [apply middle_le_le_pos | apply middle_is_in_the_middle]. apply Rabs_pos. transitivity (Rabs x) ; [apply Rabs_pos | left ; assumption]. assumption. destruct (Rpser_abs_cv_radius_weak _ _ rAn' x (proj1 (middle_is_in_the_middle _ _ x_bd))) as [l Ha']. assert (Ha := sum_r_sums An r rAn x x_bd) ; assert (Hb := sum_r_sums Bn r rBn x x_bd) ; assert (H1 := sum_r_sums (An # Bn)%Rseq r rAnBn x x_bd) ; assert (H2 := Rpser_prod_compat _ _ _ _ _ _ Ha 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