theorem CountD: :: NEWTON03:52

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