for x being integer number holds
( x |^ 2, 0 are_congruent_mod 3 or x |^ 2,1 are_congruent_mod 3 )