for a being Nat holds
( a >= 3 iff (a |^ 2) + (a |^ 2) > (a + 1) |^ 2 )