proposition: Theorem Rlt_monotony_exp : forall (x y : R) (z : Z), (x < y)%R -> (x * powerRZ radix z < y * powerRZ radix z)%R.
proof: Proof. intros x y z H'; apply Rmult_lt_compat_r; auto with real zarith. now apply powerRZ_lt, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz