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