proposition: Theorem ln_increasing : forall x y:R, 0 < x -> x < y -> ln x < ln y.
proof: Proof. intros x y H H0; apply exp_lt_inv. repeat rewrite exp_ln. - apply H0. - apply Rlt_trans with x; assumption. - apply H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra