theorem Th27: :: NUMBER17:27

for i, j being Integer st i,j are_congruent_mod j holds
i, 0 are_congruent_mod j