theorem :: ASYMPT_1:86

for n being Element of NAT st n >= 1 holds
((n + 1) / n) to_power n <= ((n + 2) / (n + 1)) to_power (n + 1) by Lm42;