proposition: Lemma weaksum_r_derive_sums : forall An r (Pr : Cv_radius_weak An r) x, Rabs x < r -> Rpser (An_deriv An) x (weaksum_r_derive An r Pr x).
proof: Proof. intros An r Pr x x_bd ; unfold weaksum_r_derive ; destruct (Rlt_le_dec (Rabs x) r) as [H | Hf]. apply weaksum_r_sums ; apply middle_is_in_the_middle ; assumption. exfalso ; lra. 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