theorem CMI: :: NEWTON06:70
for a, b being non zero Integer
for c being Integer holds (c mod (a * b)) mod a = c mod a