theorem Th31: :: NAT_3:31

for p being Prime
for a, b being non zero Nat st b divides a holds
p |-count (a div b) = (p |-count a) -' (p |-count b)