proposition: Theorem ln_mult : forall x y:R, 0 < x -> 0 < y -> ln (x * y) = ln x + ln y.
proof: Proof. intros x y H H0; apply exp_inv. rewrite exp_plus. repeat rewrite exp_ln. - reflexivity. - assumption. - assumption. - apply Rmult_lt_0_compat; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra