proposition: Lemma arctan_sum_sums : forall x, - 1 < x <= 1 -> Rpser arctan_seq x (arctan_sum x).
proof: Proof. intros x [x_lb x_ub] ; unfold arctan_sum ; destruct (MyRIneq.Req_dec x 1) as [Heq | Hneq]. subst ; rewrite <- Rmult_1_l ; apply Rpser_zip_compat_0_r. eapply Rseq_cv_eq_compat. 2: apply Rzeta2.PI_tg_PI. apply sum_f_R0_ext; intros n. change ((-1) ^ n * / INR (S (2 * n)) * (1 ^ 2) ^ n = (-1) ^ n * / INR (2 * n + 1)). rewrite 2 Rfunctions.pow1. rewrite Nat.add_comm; simpl plus; simpl mult. ring. apply sum_r_sums, Rabs_def1. apply Rneq_le_lt ; assumption. 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