for x, y, n being integer number holds
( x,y are_congruent_mod n iff ex k being Integer st x = (k * n) + y )