proposition: Lemma weaksum_r_sums : forall (An : nat -> C) (r : R) (Pr : Cv_radius_weak An r) (x : C), Cnorm x < r -> Cpser An x (weaksum_r An r Pr x).
proof: Proof. intros An r Pr x x_bd. unfold weaksum_r ; case (Rlt_le_dec (Cnorm x) r) ; intro s. destruct (Cpser_abel An r Pr x s) as (l,Hl) ; simpl ; assumption. apply False_ind ; lra. 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