for m, n being Nat st 2 <= m holds
n + 1 <= m to_power n by NEWTON:85;