theorem :: NEWTON03:93

for p being prime Nat
for a being non trivial Nat
for b being non zero Nat holds a |-count (p |^ b) <= b