theorem :: PRGCOR_1:12

for n, m being Integer holds idiv_prg (n,m) = n div m