for m, n being Nat holds m <= m to_power (n + 1)