for p being Prime
for n being non zero Element of NAT holds p |-count <*n*> = <*(p |-count n)*>