for x, y being integer number
for n being integer positive number holds
( x,y are_congruent_mod n iff x mod n = y mod n )