proposition: Lemma Vn_simpl : forall n, (0 < n)%nat -> Vn n = (INR n + / 2) * ln (1 + / INR n) - 1.
proof: Proof. intros n Hn. rewrite Vn_S; [|assumption]; unfold Un, Rseq_fact, Rdiv. assert (Hnpos : 0 < INR n). apply lt_0_INR; assumption. assert (HSnpos : 0 < INR (S n)). apply lt_0_INR; constructor; assumption. replace (1 + / INR n) with ((INR n + 1) * / INR n) by (field; auto with stirling). rewrite fact_simpl. repeat rewrite mult_INR. repeat (rewrite ln_mult || rewrite ln_Rinv); auto 6 with stirling. repeat rewrite ln_exp; auto with stirling. repeat rewrite ln_pow; auto with stirling. repeat rewrite ln_sqrt; auto with stirling. repeat rewrite S_INR. field. lra. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis