for i, k, n being Integer holds (i + (k * n)) mod n = i mod n