let m, n be Nat; :: thesis: m <= m to_power (n + 1)

per cases ( m = 0 or 1 <= m ) by NAT_1:14;

suppose m = 0 ; :: thesis: m <= m to_power (n + 1)

hence m <= m to_power (n + 1) ; :: thesis: verum

end;

suppose A1: 1 <= m ; :: thesis: m <= m to_power (n + 1)

1 <= n + 1 by NAT_1:11;
then m to_power 1 <= m to_power (n + 1) by A1, PRE_FF:8;
hence m <= m to_power (n + 1) by NEWTON:5; :: thesis: verum

end;

end;