proposition: Theorem Zle_powerRZ : forall (e : R) (n m : Z), (1 < e)%R -> (powerRZ e n <= powerRZ e m)%R -> (n <= m)%Z.
proof: Proof. intros e n m H' H'0. case (Zle_or_lt n m); auto; intros Z1. absurd (powerRZ e n <= powerRZ e m)%R; auto. apply Rlt_not_le. apply Rlt_powerRZ; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz