for b being Nat holds
( not 3 divides (b |^ 2) + 1 & not 3 divides (b |^ 2) - 2 )