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