proposition: Lemma ln1pc_exists : forall x, (0 <= x < 1)%R -> { l : R | Un_cv (sum_f_R0 (tg_alt (fun n => / INR (n + 1) * x ^ n)%R)) l }.
proof: Proof. intros x Hx. apply alternated_series. apply Un_decreasing_ln1pc. apply (conj (proj1 Hx)). now apply Rlt_le. apply Un_cv_ln1pc. rewrite Rabs_pos_eq by easy. now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)