theorem Count2: :: NEWTON03:60

for a being non trivial Nat
for b being non zero Integer
for n being non zero Nat holds
( n * (a |-count b) <= a |-count (b |^ n) & a |-count (b |^ n) < n * ((a |-count b) + 1) )