theorem Th9: :: PRGCOR_1:9

for n, m being Element of NAT st m > 0 holds
idiv1_prg (n,m) = n div m