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

per cases ( b |-count a <> 0 or b |-count a = 0 ) ;

suppose A1: b |-count a <> 0 ; :: thesis: ( b |-count a = 0 iff a mod b <> 0 )

then b divides a by MOB16;
hence ( b |-count a = 0 iff a mod b <> 0 ) by A1, PEPIN:6; :: thesis: verum

end;

suppose A1: b |-count a = 0 ; :: thesis: ( b |-count a = 0 iff a mod b <> 0 )

then not b divides a by MOB16;
hence ( b |-count a = 0 iff a mod b <> 0 ) by A1, PEPIN:6; :: thesis: verum

end;

end;