for p being Prime
for a, b being non zero Nat st b divides a holds
p |-count b <= p |-count a