proposition: Theorem Rpower_lt : forall x y z:R, 1 < x -> y < z -> Rpower x y < Rpower x z.
proof: Proof. intros x y z H H1. unfold Rpower. apply exp_increasing. apply Rmult_lt_compat_r. - rewrite <- ln_1; apply ln_increasing. + apply Rlt_0_1. + apply H. - apply H1. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra