proposition: Lemma sum_r_derive_unique : forall An r(Pr1 Pr2 : finite_cv_radius An r) z, Rabs z < r -> sum_r_derive An r Pr1 z = sum_r_derive An r Pr2 z .
proof: Proof. intros An r Pr1 Pr2 z z_bd ; assert (T1 := sum_r_derive_sums _ _ Pr1 _ z_bd) ; assert (T2 := sum_r_derive_sums _ _ Pr2 _ z_bd). eapply Rpser_unique ; eassumption. 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