for t, z being Integer holds t gcd z = (- t) gcd z