for n being natural non zero number
for x being integer number holds
not not x, 0 are_congruent_mod n & ... & not x,n - 1 are_congruent_mod n