proposition: Lemma Un_cv_atanc : forall x : R, (Rabs x <= 1)%R -> Un_cv (fun n : nat => (/ INR (2 * n + 1) * x ^ (2 * n)))%R 0.
proof: Proof. intros x Hx eps Heps. unfold R_dist. destruct (archimed_cor1 eps Heps) as [N [HN1 HN2]]. exists N. intros n Hn. assert (H: (0 < / INR (2 * n + 1))%R). apply Rinv_0_lt_compat. apply (lt_INR 0). rewrite Nat.add_comm. apply Nat.lt_0_succ. rewrite Rminus_0_r, Rabs_pos_eq. apply Rle_lt_trans with (/ INR (2 * n + 1) * 1)%R. apply Rmult_le_compat_l. now apply Rlt_le. rewrite <- (pow1 (2 * n)). apply pow_maj_Rabs with (1 := Hx). rewrite Rmult_1_r. apply Rlt_trans with (2 := HN1). apply Rinv_lt. now apply (lt_INR 0). apply lt_INR. apply Nat.le_lt_trans with (1 := Hn). clear ; lia. apply Rmult_le_pos. now apply Rlt_le. rewrite pow_Rsqr. apply pow_le. apply Rle_0_sqr. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)