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