theorem :: NEWTON03:72

for a being non trivial Nat
for n, b being non zero Nat holds a |-count b >= n * ((a |^ n) |-count b)