proposition: Lemma finite_cv_radius_ext : forall r, finite_cv_radius An r <-> finite_cv_radius Bn r.
proof: Proof. intro r ; split ; intros [rho_lb rho_ub] ; split ; intros r' Hr' ; [rewrite <- Cv_radius_weak_ext | rewrite <- Cv_radius_weak_ext | rewrite Cv_radius_weak_ext | rewrite Cv_radius_weak_ext] ; auto. 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