for i, j, k being Integer st i,j are_coprime holds
i gcd (j * k) = i gcd k