for m, n being non zero Nat st ( for p being Prime holds p |-count m <= p |-count n ) holds
m divides n