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