proposition: Lemma Rpser_abs_infinite_cv_radius: forall An, infinite_cv_radius An -> forall x, {l | Rpser_abs An x l}.
proof: Proof. intros An rAn x ; apply (Rpser_abs_cv_radius_weak _ _ (rAn (Rabs x + 1)) x (Rlt_n_Sn _)). Qed.
imports: Reals Fourier Lra Rpow_facts Rinterval Rextensionality Rsequence_facts Rsequence_sums_facts Rsequence_rewrite_facts RFsequence RFsequence_facts Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_sums MyINR