let b be non trivial Nat; :: thesis: for a being non zero Integer holds
( b |-count a <> 0 iff b divides a )
let a be non zero Integer; :: thesis: ( b |-count a <> 0 iff b divides a )
( b |-count |.a.| <> 0 iff b divides |.a.| )

proof

( b <> 1 & a <> 0 ) by NAT_2:def 1;
hence ( b |-count |.a.| <> 0 iff b divides |.a.| ) by NAT_3:27; :: thesis: verum

end;

hence ( b |-count a <> 0 iff b divides a ) by INT_2:16; :: thesis: verum