proposition: Lemma identite : forall k b : nat, (k > b)%nat -> INR (fact b) * / INR (fact k) <= / INR (S b) * (/ INR (S b)) ^ (k - S b).
proof: Proof. intros k n Hnb. induction Hnb. rewrite fact_simpl. rewrite mult_INR. replace (S n - S n)%nat with O by intuition. simpl pow. field_simplify. right. reflexivity. apply not_0_INR. intuition. split. apply INR_fact_neq_0. apply not_0_INR. intuition. rewrite fact_simpl. rewrite mult_INR. rewrite Nat.sub_succ_l ; [|intuition]. assert (/INR (S m) <= /INR (S n)) by (apply Rle_Rinv ; intuition) . rewrite <- tech_pow_Rmult. rewrite Rinv_mult_distr. rewrite Rmult_comm. rewrite Rmult_assoc. apply Rmult_le_compat. left. apply Rinv_0_lt_compat. intuition. left. rewrite Rmult_comm. apply Rlt_mult_inv_pos ; apply INR_fact_lt_0. apply Rle_Rinv ; [apply lt_0_INR ; intuition|apply lt_0_INR ; intuition|intuition]. rewrite Rmult_comm. apply IHHnb. apply not_0_INR. intuition. apply INR_fact_neq_0. Qed.
imports: PeanoNat Rseries_facts Rsequence_facts Rsequence_subsequence Rpser_usual Reals Rsequence_tactics Rtactic Lra