proposition: Lemma infinite_cv_radius_subseq_compat : forall An Bn, subsequence Bn An -> infinite_cv_radius An -> infinite_cv_radius Bn.
proof: Proof. intros An Bn HAB HAn r ; pose (r' := Rmax (Rabs r) 1) ; assert (r'_pos : 0 <= r') by (apply Rmax_pos_l, Rabs_pos). apply Cv_radius_weak_le_compat with r'. rewrite (Rabs_right r') ; [apply Rmax_l | apply Rle_ge ; assumption]. eapply Cv_radius_weak_subseq_compat. rewrite (Rabs_right r') ; [apply Rmax_r | apply Rle_ge ; assumption]. eassumption. apply HAn. 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