theorem Th10: :: PRGCOR_1:10

for n, m being Integer st n >= 0 & m > 0 holds
idiv1_prg (n,m) = n div m