proposition: Theorem Rle_pow : forall (e : R) (n m : nat), (1 < e)%R -> n <= m -> (e ^ n <= e ^ m)%R.
proof: Proof. intros e n m H H0; case (proj1 (Nat.lt_eq_cases _ _) H0); auto with real. intros H1; rewrite H1; auto with real. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)