theorem LMC31B: :: ASYMPT_2:2

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