proposition: Lemma Un_cv_ln1pc : forall x : R, (Rabs x <= 1)%R -> Un_cv (fun n : nat => (/ INR (n + 1) * x ^ 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 (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. rewrite Rabs_mult, Rabs_pos_eq. apply Rle_lt_trans with (/ INR (n + 1) * 1)%R. apply Rmult_le_compat_l. now apply Rlt_le. rewrite <- (pow1 n). rewrite <- RPow_abs. apply pow_maj_Rabs. now rewrite Rabs_Rabsolu. 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). rewrite Nat.add_comm. apply Nat.lt_succ_diag_r. now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)