theorem :: ASYMPT_1:78

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