proposition: Theorem ln_Rinv : forall x:R, 0 < x -> ln (/ x) = - ln x.
proof: Proof. intros x H; apply exp_inv; repeat rewrite exp_ln || rewrite exp_Ropp. - reflexivity. - assumption. - apply Rinv_0_lt_compat; assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra