let a, b be Nat; ( b <> 0 & b < a & a <> 1 implies a |-count b = 0 )
assume that
A1:
b <> 0
and
A2:
b < a
and
A3:
a <> 1
; a |-count b = 0
a |^ 0 = 1
by NEWTON:4;
then A4:
a |^ 0 divides b
by NAT_D:6;
not a |^ (0 + 1) divides b
by A1, A2, NAT_D:7;
hence
a |-count b = 0
by A1, A3, A4, Def7; verum