theorem Th12: :: NAT_6:12

for i, j being integer number
for n being natural number st n < j & i,n are_congruent_mod j holds
i mod j = n