theorem CountD1: :: NEWTON03:53

for n being Nat
for b being non zero Integer
for a being Integer st |.a.| <> 1 & a |^ n divides b & not a |^ (n + 1) divides b holds
n = |.a.| |-count |.b.|