for m, n being Nat
for p being Prime st n <> 0 & m <= p |-count n holds
p |^ m divides n