theorem NAT327: :: NEWTON03:77

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