proposition: Lemma identite1 : forall b, INR (fact b) * / INR (fact (S (S b))) < / INR (S b) * (/ INR (S b)) ^ (S (S b) - S b).
proof: Proof. intros b. do 2 rewrite fact_simpl. rewrite Nat.sub_succ_l ; [|intuition]. rewrite Nat.sub_diag. rewrite <- tech_pow_Rmult. simpl pow. do 2 rewrite mult_INR. field_simplify. unfold Rdiv. rewrite Rinv_mult_distr. unfold pow. rewrite Rinv_mult_distr. do 2 rewrite Rmult_1_l. rewrite Rmult_1_r. apply Rmult_lt_compat_r. apply Rinv_0_lt_compat. intuition. apply Rinv_lt_contravar. apply Rmult_lt_0_compat ; intuition. intuition. apply not_0_INR. intuition. rewrite Rmult_1_r. apply not_0_INR. intuition. apply not_0_INR. intuition. apply not_0_INR. intuition. apply not_0_INR. intuition. split. apply INR_fact_neq_0. split. apply not_0_INR. intuition. apply not_0_INR. intuition. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra