proposition: Lemma Cv_radius_weak_subseq_compat : forall An Bn r, 1 <= Rabs r -> subsequence Bn An -> Cv_radius_weak An r -> Cv_radius_weak Bn r.
proof: Proof. intros An Bn r Hr [[phi Hphi] HAB] [ub Hub]. exists ub ; intros B [i Hi] ; subst ; transitivity (gt_abs_pser An r (phi i)). unfold gt_abs_pser, Rseq_abs, gt_pser, Rseq_mult ; do 2 rewrite Rabs_mult. apply Rmult_le_compat ; try (apply Rabs_pos). right ; apply Rabs_eq_compat, HAB. do 2 rewrite <- RPow_abs ; apply Rle_pow, Rsubseq_n_le_extractor_n ; assumption. apply Hub ; exists (phi 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