proposition: Lemma derivable_Rball_weaksum_r: forall An r (rho : Cv_radius_weak An r), derivable_Rball 0 r (weaksum_r An r rho).
proof: Proof. intros An r rho x x_in ; apply derivable_pt_in_weaksum_r ; assumption. Qed.
imports: Reals Rpow_facts Rfunction_def Rinterval Rextensionality Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Lra MyRIneq Rsequence_facts Rsequence_sums_facts RFsequence RFsequence_facts Rpser_def Rpser_base_facts Rpser_radius_facts Rpser_sums Rpser_sums_facts Tactics