proposition: Lemma sum_pow_cv_radius : finite_cv_radius sum_pow_seq 1.
proof: Proof. rewrite <- Rinv_1 ; apply Rpser_alembert_finite. apply Rgt_not_eq, Rlt_0_1. intro ; apply Rgt_not_eq, Rlt_0_1. eapply Rseq_cv_eq_compat, Rseq_constant_cv. intro ; unfold sum_pow_seq, Rseq_abs, Rseq_div, Rseq_shift, Rseq_constant, Rdiv. rewrite Rinv_1, Rmult_1_r ; apply Rabs_R1. Qed.
imports: MyReals MyINR MyNNR Rsequence_def Rsequence_facts Rsequence_cv_facts Rsequence_sums_facts Rsequence_base_facts Rsequence_rewrite_facts Rsequence_usual_facts Rsequence_subsequence PeanoNat Lra Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_cv_facts Rpser_radius_facts Rpser_sums Rpser_derivative Rpser_derivative_facts Rfunction_def Functions Rextensionality Rpow_facts Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity