proposition: Lemma weaksum_r_scal_compat : forall (k: R) (rAn' : Cv_radius_weak (k * An)%Rseq r), weaksum_r (k * An)%Rseq r rAn' x = ((fun _ => k) * weaksum_r An r rAn)%F x.
proof: Proof. intros k rAn'. assert (H1 := weaksum_r_sums _ _ rAn' x x_bd) ; assert (H2 := Rpser_scal_compat k _ _ _ (weaksum_r_sums _ _ rAn x x_bd)) ; eapply Rpser_unique ; unfold mult_fct ; 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