proposition: Lemma infinite_cv_radius_zip_compat_l : infinite_cv_radius (Rseq_zip An Bn).
proof: Proof. intro r ; apply Cv_radius_weak_Rabs ; rewrite <- Rsqrt_sqr with (y := nnr_sqr (Rabs r)). apply Cv_radius_weak_zip_l ; [apply rAn | apply rBn]. apply Rabs_pos. 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