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

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