for t, u, z being Integer holds
( (t + (u * z)) gcd z = t gcd z & (t - (u * z)) gcd z = t gcd z )