theorem Th14: :: NUMERAL2:14

for i, j being Integer holds (i mod j) mod j = i mod j