for i1, i2 being Integer st i2 <> 0 holds
i1 = ((i1 div i2) * i2) + (i1 mod i2)