let n, m, l be Element of NAT ; :: thesis: ( n divides m & n divides l implies n divides m - l )
assume A1: ( n divides m & n divides l ) ; :: thesis: n divides m - l
then A2: m = n * (m div n) by NAT_D:3;
- l = - (n * (l div n)) by A1, NAT_D:3
.= n * (- (l div n)) ;
then m - l = n * ((m div n) + (- (l div n))) by A2;
hence n divides m - l by INT_1:def 9; :: thesis: verum