proposition: Lemma arctan_cv_radius : finite_cv_radius arctan_seq 1.
proof: Proof. rewrite <- Rsqrt_sqr with (y := nnr_sqr 1) ; [| lra | simpl ; ring]. apply finite_cv_radius_zip_compat_r. intros ; apply zero_infinite_cv_radius. simpl nonneg ; do 2 rewrite Rmult_1_r ; rewrite <- finite_cv_radius_alt_compat ; apply arct_cv_radius. 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