proposition: Theorem ln_exp : forall x:R, ln (exp x) = x.
proof: Proof. intros x; apply exp_inv. apply exp_ln. apply exp_pos. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra