theorem :: ASYMPT_1:79

for n being Element of NAT st n >= 1 holds
n ^2 <= 2 * (((n ^2) - n) + 1) by Lm24;