proposition: Theorem exp_increasing : forall x y:R, x < y -> exp x < exp y.
proof: Proof. intros x y H. assert (H0 : derivable exp). - apply derivable_exp. - assert (H1 := positive_derivative _ H0). unfold strict_increasing in H1. apply H1. + intro. replace (derive_pt exp x0 (H0 x0)) with (exp x0). * apply exp_pos. * symmetry ; apply derive_pt_eq_0. apply (derivable_pt_lim_exp x0). + apply H. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra