proposition: Lemma ln_sqrt : forall r, 0 < r -> ln (sqrt r) = ln r / 2.
proof: Proof. intros r Hr. assert (H : 2 <> 0). intros Hc; lra. unfold Rdiv; rewrite Rmult_comm. apply (Rmult_eq_reg_l 2); [|assumption]. rewrite <- Rmult_assoc. rewrite Rinv_r; [|assumption]. rewrite Rmult_1_l. replace 2 with (INR 2) by reflexivity. rewrite <- ln_pow. replace (sqrt r ^ 2) with (sqrt r * sqrt r) by field. rewrite sqrt_def; [reflexivity|lra]. apply sqrt_lt_R0; assumption. Qed.
imports: Reals Rsequence_facts Rseries_def Rseries_facts Rseries_usual Rpser Rintegral RTaylor Lia Lra Wallis