let a, b, i be Integer; :: thesis: ( i divides a & i divides a - b implies i divides b )
assume that
A1: i divides a and
A2: i divides a - b ; :: thesis: i divides b
A3: b = (- (a - b)) + a ;
i divides - (a - b) by A2, INT_2:10;
hence i divides b by A1, A3, WSIERP_1:4; :: thesis: verum