for a, b, n being Nat st n > 0 holds
(a gcd b) gcd (b |^ n) = a gcd b