proposition: Lemma Rle_Cv_radius_weak_compat : forall (An Bn : nat -> R) (r : R), (forall n, Rabs (Bn n) <= Rabs (An n)) -> Cv_radius_weak An r -> Cv_radius_weak Bn r.
proof: Proof. intros An Bn r Bn_le_An [M HM] ; exists M ; intros x [n Hn] ; subst ; apply Rle_trans with (gt_abs_pser An r n) ; [| apply HM ; exists n ; reflexivity]. unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult ; do 2 rewrite Rabs_mult ; apply Rmult_le_compat_r ; [apply Rabs_pos | apply Bn_le_An]. 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