proposition: Lemma exp_ln : forall x:R, 0 < x -> exp (ln x) = x.
proof: Proof. intros; unfold ln; decide (Rlt_dec 0 x) with H. unfold Rln; case (ln_exists (mkposreal x H) (cond_pos (mkposreal x H))) as (?,Hex). symmetry; apply Hex. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra