theorem Count1: :: NEWTON03:59

for n being Nat
for a being non trivial Nat
for b being non zero Integer holds
( a |^ n divides b iff n <= a |-count b )