for a, b being Integer
for n being Nat holds ((a mod n) + (b mod n)) mod n = (a + (b mod n)) mod n