proposition: Theorem Rle_powerRZ : forall (e : R) (n m : Z), (1 <= e)%R -> (n <= m)%Z -> (powerRZ e n <= powerRZ e m)%R.
proof: Proof. intros e n m H' H'0. case H'; intros E1. case (Zle_lt_or_eq _ _ H'0); intros E2. apply Rlt_le; auto with real. now apply Rlt_powerRZ. rewrite <- E2; auto with real. repeat rewrite <- E1; repeat rewrite powerRZ_R1; auto with real. Qed.
imports: Reals ZArith List PeanoNat Psatz