for a, b being Nat st b |^ 2 = a * (a - b) holds
( 3 divides a & 3 divides b )