proposition: Theorem Rle_Rpower : forall e n m:R, 1 <= e -> n <= m -> Rpower e n <= Rpower e m.
proof: Proof. intros e n m [H | H]; intros H1. - case H1. + intros H2; left; apply Rpower_lt; assumption. + intros H2; rewrite H2; right; reflexivity. - now rewrite <- H; unfold Rpower; rewrite ln_1, !Rmult_0_r; apply Rle_refl. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 Exp_prop Rsqrt_def R_sqrt Sqrt_reg MVT Ranalysis4 Lra