proposition: Lemma identity_infinite_cv_radius : infinite_cv_radius identity_seq.
proof: Proof. intros r ; exists (Rabs r) ; intros x [i Hi] ; subst ; unfold gt_abs_pser, gt_pser, Rseq_abs, Rseq_mult, identity_seq ; destruct (eq_nat_dec i 1) as [Heq|Hneq]. rewrite Heq ; right ; apply Rabs_eq_compat ; ring. rewrite Rmult_0_l, Rabs_R0 ; apply Rabs_pos. 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