for k, p, n being Nat st p is prime & n < p |^ (k + 1) holds
( n divides p |^ (k + 1) iff n divides p |^ k )