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