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