proposition: Lemma sum_derive_unique : forall (An : nat -> R) (Pr1 Pr2 : infinite_cv_radius An) (z : R), sum_derive An Pr1 z = sum_derive An Pr2 z .
proof: Proof. intros An Pr1 Pr2 z ; assert (T1 := sum_derive_sums _ Pr1 z) ; assert (T2 := sum_derive_sums _ Pr2 z). 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