proposition: Theorem Rle_monotone_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_le_compat_r; auto with real zarith. now apply powerRZ_le, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz