proposition: Lemma Stirling_equiv : Rseq_fact ~ (fun n => sqrt (2 * PI) * (INR n) ^ n * exp (- (INR n)) * sqrt (INR n)).
proof: Proof. destruct De_Moivre_equiv as [l Hl]. assert(l^2/(2*PI) = 1) as Heq. eapply Rseq_cv_unique. apply Wallis_quotient_lim2. auto with *. assert (Hrw : (fun n => l * n ^ n * exp (-n) * sqrt n) == (fun n => ((n / exp R1) ^ n * sqrt n * l))). intro n. rewrite exp_Ropp. replace (exp n) with (exp (R1*n)) by auto with *. rewrite <- (exp_pow R1 n). unfold Rdiv; rewrite Rpow_mult_distr, Rinv_pow. field. assert (H := exp_pos 1); auto with *. eapply Rseq_equiv_eq_compat. apply Rseq_eq_refl. apply Hrw. trivial. apply Wallis_quotient_lim1. replace l with (sqrt(2*PI)) in Hl. apply Hl. assert(HPI := PI_RGT_0). apply sqrt_lem_1. lra. auto with *. replace (l*l) with ((l^2 / (2*PI))* (2*PI)). rewrite Heq; ring. unfold Rdiv, Rsqr; field; auto with *. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis