for b, n being non zero Nat
for a being non trivial Nat holds
( a |-count (a gcd b) = 1 iff (a |^ n) |-count ((a gcd b) |^ n) = 1 )