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