let a, b, c be Integer; :: thesis: ( a = b mod c & c <> 0 implies ex d being Element of INT st a = b + (d * c) )

assume ( a = b mod c & c <> 0 ) ; :: thesis: ex d being Element of INT st a = b + (d * c)

then A1: b = ((b div c) * c) + a by INT_1:59;

reconsider x = - (b div c) as Element of INT by INT_1:def 2;

take x ; :: thesis: a = b + (x * c)

thus a = b + (x * c) by A1; :: thesis: verum

assume ( a = b mod c & c <> 0 ) ; :: thesis: ex d being Element of INT st a = b + (d * c)

then A1: b = ((b div c) * c) + a by INT_1:59;

reconsider x = - (b div c) as Element of INT by INT_1:def 2;

take x ; :: thesis: a = b + (x * c)

thus a = b + (x * c) by A1; :: thesis: verum