proposition: Lemma ln_pow : forall r n, 0 < r -> ln (r ^ n) = INR n * ln r.
proof: Proof. intros r n Hr; induction n. simpl; rewrite ln_1; rewrite Rmult_0_l; auto. replace (r ^ S n) with (r * r ^ n) by reflexivity. rewrite ln_mult. rewrite S_INR; rewrite IHn; field. assumption. apply pow_lt; assumption. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis