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