not a divides 1 by NAT_D:7, NEWTON03:def 1;
hence a |-count 1 is zero by NEWTON03:77; :: thesis: verum