fact: Definition ps_atan_exists_1 (x : R) (Hx : -1 <= x <= 1) : {l : R | Un_cv (fun N : nat => sum_f_R0 (tg_alt (Ratan_seq x)) N) l}.
imports: Lra Rbase PSeries_reg Rtrigo1 Rtrigo_facts Ranalysis_reg Rfunctions AltSeries Rseries SeqProp Ranalysis5 SeqSeries PartSum Lia