proposition: Lemma infinite_cv_radius_zip_compat_r2 : forall An Bn, infinite_cv_radius (Rseq_zip An Bn) -> infinite_cv_radius Bn.
proof: Proof. intros An Bn rAnBn r ; apply Cv_radius_weak_Rabs ; replace (Rabs r) with (nonneg (nnr_abs r)) by reflexivity ; rewrite <- Rsqr_Rsqrt with (nnr_abs r). eapply Cv_radius_weak_zip_r2, rAnBn. 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