proposition: Lemma Vn_ser_eq : forall n, sum_f_R0 Vn n = ln (Un (S n)) - ln (Un 1).
proof: Proof. intros n. induction n. unfold Vn; simpl; ring. simpl sum_f_R0; rewrite IHn. unfold Rdiv; rewrite ln_mult. rewrite ln_Rinv; [ring|]. apply Un_pos; lia. apply Un_pos; lia. apply Rinv_0_lt_compat; apply Un_pos; lia. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis