for p, q, n being Nat st n > 0 & p is prime & p,q are_coprime holds
not p divides q mod (p |^ n)