theorem Count0: :: NEWTON03:58

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