for n being natural non zero number
for x being integer number
for k, l being natural number st k < n & l < n & x,k are_congruent_mod n & x,l are_congruent_mod n holds
k = l