proposition: Lemma infinite_cv_radius_zero : infinite_cv_radius 0.
proof: Proof. intro r ; exists 0 ; intros x [n Hn] ; subst ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult, Rseq_constant ; rewrite Rmult_0_l, Rabs_R0 ; 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