theorem Th91: :: NEWTON02:189
for b, c being Nat st not 3 divides b holds
not 3 divides (b |^ 2) + (c |^ 2)