for i1, i2, i3 being Integer st i3 <> 0 holds
( i1 divides i2 iff i1 * i3 divides i2 * i3 )