proposition: Lemma ln_neq_0 : forall x:R, x <> 1 -> 0 < x -> ln x <> 0.
proof: Proof. intros x Hneq_x_1 Hlt_0_x. rewrite <- ln_1. intro H. assert (x = 1) as H0. + exact (ln_inv x 1 Hlt_0_x (ltac:(lra) : 0 < 1) H). + contradiction. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra