theorem Th51: :: NAT_4:52

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