proposition: Lemma De_Moivre_equiv : {C | Rseq_fact ~ (fun n => C * (INR n) ^ n * exp (- (INR n)) * sqrt (INR n)) & 0 < C}.
proof: Proof. destruct Un_cv as [l Hl Hp]. exists (/ l). apply Rseq_equiv_sym. apply Rseq_equiv_1. intros n; apply not_0_INR. apply fact_neq_0. apply Rseq_equiv_sym. intros eps Heps. destruct (Hl (eps * / 2 * l)) as [N HN]. apply Rmult_lt_0_compat; [lra|assumption]. exists N; intros n Hn. unfold Rseq_constant, Rseq_minus, Rseq_div. rewrite (Rabs_right 1); [|lra]. rewrite Rmult_1_r. rewrite Rabs_minus_sym. apply Rle_trans with (eps / 2); [left|lra]. apply (Rmult_lt_reg_l l); [assumption|]. pattern l at 1; rewrite <- Rabs_right; [|lra]. rewrite <- Rabs_mult. rewrite (Rmult_comm l (eps / 2)). replace (l * (/ l * INR n ^ n * exp (- INR n) * sqrt (INR n) / Rseq_fact n - 1)) with (INR n ^ n * exp (- INR n) * sqrt (INR n) / Rseq_fact n - l). apply HN; assumption. field; split. intro; lra. apply not_0_INR; apply fact_neq_0. apply Rinv_0_lt_compat; assumption. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis