proposition: Lemma infinite_cv_radius_abs_compat : forall (An : Rseq), infinite_cv_radius An <-> infinite_cv_radius (| An |).
proof: Proof. intros An ; split ; intros rho r ; [rewrite <- Cv_radius_weak_abs | rewrite Cv_radius_weak_abs] ; apply rho. 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