for p being Prime
for n being non zero Nat holds
( p divides n iff p |-count n > 0 )