for b being non trivial Nat
for a being non zero Nat holds
( b |-count a = 0 iff a mod b <> 0 )