theorem Th23: :: NAT_3:23

for a, b being Nat st b <> 0 & b < a & a <> 1 holds
a |-count b = 0