proposition: Lemma arctan_sum_0_0 : arctan_sum 0 = 0.
proof: Proof. eapply Rpser_unique ; [eapply arctan_sum_sums |]. split ; lra. apply Rseq_cv_eq_compat with (fun _ => 0). intro ; rewrite Rseq_pps_0_simpl ; unfold arctan_seq, Rseq_zip. case (n_modulo_2 0) ; intros [p Hp] ; [reflexivity | apply False_ind ; lia ]. apply Rseq_constant_cv. 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