proposition: Lemma Cv_radius_weak_le_compat : forall (An : nat -> R) (r r' : R), Rabs r' <= Rabs r -> Cv_radius_weak An r -> Cv_radius_weak An r'.
proof: Proof. intros An r r' r'_bd [B HB]. exists B ; intros x [i Hi] ; subst ; apply Rle_trans with (gt_abs_pser An r i). apply gt_abs_pser_le_compat ; assumption. apply HB ; exists i ; reflexivity. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR