let n, m, l be Nat; :: thesis: ( n divides m & n divides l implies n divides m - l )
assume that
A1: n divides m and
A2: n divides l ; :: thesis: n divides m - l
A3: - l = - (n * (l div n)) by A2, NAT_D:3
.= n * (- (l div n)) ;
m = n * (m div n) by A1, NAT_D:3;
then m - l = n * ((m div n) + (- (l div n))) by A3;
hence n divides m - l by INT_1:def 3; :: thesis: verum