theorem :: ASYMPT_1:90

for n being Element of NAT st n >= 2 holds
n ^2 > n + 1 by Lm47;