theorem MOB16: :: NEWTON03:89

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