proposition: Lemma sum_r_arctan_explicit : forall x, Rball 0 1 x -> sum_r _ _ arctan_cv_radius x = x * sum_r _ _ arct_cv_radius (- x ^ 2).
proof: Proof. intros x x_in ; assert (x_bd : Rabs x < 1) by (rewrite <- Rball_0_simpl ; apply x_in). assert (x2_bd : Rabs (x ^ 2) < 1). rewrite <- RPow_abs ; apply Rpow_lt_1_compat ; [apply Rabs_pos | assumption]. eapply eq_trans ; [apply sum_r_zip_compat_0_r with (rAn := proj1 (finite_cv_radius_alt_compat _ _) arct_cv_radius) ; assumption |]. apply Rmult_eq_compat_l, sum_r_alt_compat ; assumption. 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 Rpser_sums_facts