theorem :: RADIX_1:7

for i1, i2, i3 being Integer st i2 > 0 & i3 >= 0 holds
(i1 mod (i2 * i3)) mod i3 = i1 mod i3