proposition: Lemma Un_decreasing_ln1pc : forall x : R, (0 <= x <= 1)%R -> Un_decreasing (fun n : nat => (/ INR (n + 1) * x ^ n))%R.
proof: Proof. intros x Hx n. change (S n) with (1 + n) at 2. rewrite pow_add. simpl (pow x 1). rewrite Rmult_1_r, <- Rmult_assoc. apply Rmult_le_compat_r. now apply pow_le. rewrite <- (Rmult_1_r (/ INR (n + 1))). apply Rmult_le_compat ; try easy. apply Rlt_le. apply Rinv_0_lt_compat. apply (lt_INR 0). apply Nat.lt_0_succ. apply Rlt_le. apply Rinv_lt. apply (lt_INR 0). rewrite Nat.add_comm. apply Nat.lt_0_succ. apply lt_INR. apply Nat.lt_succ_diag_r. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)