proposition: Lemma Un_decreasing_atanc : forall x : R, (Rabs x <= 1)%R -> Un_decreasing (fun n : nat => (/ INR (2 * n + 1) * x ^ (2 * n)))%R.
proof: Proof. intros x Hx n. replace (2 * S n) with (2 + 2 * n) by ring. rewrite pow_add. rewrite <- Rmult_assoc. apply Rmult_le_compat_r. rewrite pow_sqr. apply pow_le. apply Rle_0_sqr. rewrite <- (Rmult_1_r (/ INR (2 * n + 1))). apply Rmult_le_compat. apply Rlt_le. apply Rinv_0_lt_compat. apply (lt_INR 0). apply Nat.lt_0_succ. unfold pow. rewrite Rmult_1_r. apply Rle_0_sqr. apply Rlt_le. apply Rinv_lt. apply (lt_INR 0). rewrite Nat.add_comm. apply Nat.lt_0_succ. apply lt_INR. rewrite <- Nat.add_assoc. rewrite <-Nat.add_0_l at 1. rewrite <-Nat.add_lt_mono_r. apply Nat.lt_0_succ. rewrite <- (pow1 2). apply pow_maj_Rabs with (1 := Hx). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)