theorem RMI: :: NEWTON06:50

for a, b being Nat
for c, d being non zero Nat st a mod (c * d) = b mod (c * d) holds
a mod c = b mod c