for a, b being Nat st b <> 1 holds
( ( a <> 0 & b |-count a = 0 ) iff not b divides a )