let n, m be Integer; :: thesis: ( n >= 0 & m > 0 implies idiv1_prg n,m = n div m )
assume A1: ( n >= 0 & m > 0 ) ; :: thesis: idiv1_prg n,m = n div m
then reconsider n2 = n, m2 = m as Element of NAT by INT_1:16;
idiv1_prg n,m = n2 div m2 by A1, Th9;
hence idiv1_prg n,m = n div m ; :: thesis: verum