theorem Th12: :: NAT_6:12

for i, j being Integer
for n being Nat st n < j & i,n are_congruent_mod j holds
i mod j = n