for a being Nat
for p being Prime st a <> 1 & a <> p holds
a |-count p = 0