proposition: Lemma atanc_exists : forall x, (Rabs x <= 1)%R -> { l : R | Un_cv (sum_f_R0 (tg_alt (fun n => / INR (2 * n + 1) * x ^ (2 * n))%R)) l }.
proof: Proof. intros x Hx. apply alternated_series. now apply Un_decreasing_atanc. now apply Un_cv_atanc. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)