for p being prime Nat
for a being non trivial Nat holds a |-count p <= 1