let a, b, n be Nat; :: thesis: ( a < n & b < n & n divides a - b implies a = b )
assume that
A1: a < n and
A2: b < n and
A3: n divides a - b ; :: thesis: a = b
A4: n divides - (a - b) by A3, INT_2:10;
assume a <> b ; :: thesis: contradiction
then ( a > b or b > a ) by XXREAL_0:1;
then ( a - b > 0 or b - a > 0 ) by XREAL_1:50;
then ( n <= a - b or n <= b - a ) by A3, A4, INT_2:27;
then ( a < a - b or b < b - a ) by A1, A2, XXREAL_0:2;
hence contradiction by XREAL_1:43; :: thesis: verum