proposition: Lemma Cv_radius_weak_0 : forall An, Cv_radius_weak An 0.
proof: Proof. intro An ; exists (Rabs(An O)) ; intros x [n Hn] ; subst ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult. destruct n. simpl ; rewrite Rmult_1_r ; reflexivity. rewrite pow_i ; [| lia] ; rewrite Rmult_0_r, Rabs_R0 ; apply Rabs_pos. 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