proposition: Lemma sum_r_unique : forall (An : nat -> C) (r : R) (Pr1 Pr2 : finite_cv_radius An r) (x : C), Cnorm x < r -> sum_r An r Pr1 x = sum_r An r Pr2 x.
proof: Proof. intros An r Pr1 Pr2 x x_bd ; assert (T1 := sum_r_sums _ _ Pr1 _ x_bd) ; assert (T2 := sum_r_sums _ _ Pr2 _ x_bd) ; eapply Pser_unique ; eassumption. Qed.
imports: Rinterval Ranalysis_def Rpser_def Rpser_base_facts Rpser_cv_facts Rpser_sums Rpow_facts Rsequence_def Rsequence_facts Rseries_def Rseries_facts RFsequence_facts Cpow Cpser_def Cpser_base_facts CFsequence CFsequence_facts Csequence Csequence_def Csequence_facts Cmet Cnorm Ctacfield Cprop_base Canalysis_def Canalysis_cont Canalysis_deriv Canalysis_basic_facts