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