for t, u, z being Integer holds
( t * u divides z * u iff |.u.| * (t gcd z) = |.u.| * |.t.| )