for i being integer number
for j being non zero integer number holds i,i mod j are_congruent_mod j