for n being Nat
for a being non trivial Nat
for b being non zero Nat st b < a |^ n holds
a |-count b < n