let i1, i2, i3 be Integer; :: thesis: ( i1 divides i2 & i1 divides i3 implies i1 divides i2 - i3 )
assume that
A1: i1 divides i2 and
A2: i1 divides i3 ; :: thesis: i1 divides i2 - i3
consider i4 being Integer such that
A3: i2 = i1 * i4 by A1;
consider i5 being Integer such that
A4: i3 = i1 * i5 by A2;
i2 - i3 = i1 * (i4 - i5) by A3, A4;
hence i1 divides i2 - i3 ; :: thesis: verum