proposition: Lemma Ratan_is_ps_atan : forall eps, eps > 0 -> exists N, forall n, (n >= N)%nat -> forall x, -1 < x -> x < 1 -> Rabs (sum_f_R0 (tg_alt (Ratan_seq x)) n - ps_atan x) < eps.
proof: Proof. intros eps ep. destruct (Ratan_CVU _ ep) as [N1 PN1]. exists N1; intros n nN x xm1 x1; rewrite <- Rabs_Ropp, Ropp_minus_distr. apply PN1; [assumption | ]. unfold Boule; simpl; rewrite Rminus_0_r; apply Rabs_def1; assumption. Qed.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia