theorem :: ASYMPT_1:90

for n being Nat st n >= 2 holds
n ^2 > n + 1 by Lm47;