proposition: Lemma weaksum_r_ext : forall (r : R) (rAn : Cv_radius_weak An r) (rBn : Cv_radius_weak Bn r), weaksum_r An r rAn == weaksum_r Bn r rBn.
proof: Proof. intros r rAn rBn x. unfold weaksum_r ; destruct (Rlt_le_dec (Rabs x) r) ; trivial. destruct (Rpser_abel _ _ rAn x r0) as [l1 Hl1] . pose proof Hl1 as Hl0. rewrite Pser_ext in Hl0. destruct (Rpser_abel _ _ rBn x r0) as [l2 Hl2]. simpl ; eapply Rpser_unique ; eassumption. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts Rinterval Ranalysis_def Rfunction_facts Tactics