for i, j being Integer holds (i * j) gcd i = |.i.|