proposition: Lemma arctan_sum_explicit : forall x, Rball 0 1 x -> arctan_sum x = x * sum_r _ _ arct_cv_radius (- x ^ 2).
proof: Proof. intros x x_in ; unfold arctan_sum ; destruct (MyRIneq.Req_dec x 1). subst ; destruct (Rlt_irrefl 1) ; rewrite Rball_0_simpl, Rabs_R1 in x_in ; apply x_in. apply sum_r_arctan_explicit ; 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