proposition: Lemma Un_decreasing_sinc : forall x : R, (Rabs x <= 1)%R -> Un_decreasing (fun n : nat => (/ INR (fact (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. change (fact (2 + 2 * n + 1)) with ((2 + 2 * n + 1) * ((1 + 2 * n + 1) * fact (2 * n + 1))). rewrite Nat.mul_assoc, Nat.mul_comm. rewrite mult_INR. rewrite <- (Rmult_1_r (/ INR (fact _))). rewrite Rinv_mult_distr. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rlt_le. apply Rinv_0_lt_compat. apply (lt_INR 0). apply lt_O_fact. rewrite <- (Rmult_1_r 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. rewrite <- Rinv_1. apply Rle_Rinv_pos. apply Rlt_0_1. apply (le_INR 1). apply le_n_S, le_0_n. rewrite <- (pow1 2). apply pow_maj_Rabs with (1 := Hx). apply INR_fact_neq_0. now apply not_0_INR. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)