for a being non zero Integer
for b being non trivial Nat holds
( b |-count a = 0 iff not b divides a )