proposition: Theorem ln_lt_inv : forall x y:R, 0 < x -> 0 < y -> ln x < ln y -> x < y.
proof: Proof. intros x y H H0 H1; rewrite <- (exp_ln x); try rewrite <- (exp_ln y). - apply exp_increasing; apply H1. - assumption. - assumption. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra