for a being Nat
for b being non zero Nat st a > b holds
ex p being prime Nat st p |-count a > p |-count b