theorem Th30: :: NAT_3:30

for p being Prime
for a, b being non zero Nat st b divides a holds
p |-count b <= p |-count a