let a, b be Integer; :: thesis: ( b <> 0 implies a mod b,a are_congruent_mod b )

assume b <> 0 ; :: thesis: a mod b,a are_congruent_mod b

then A1: a mod b = a - ((a div b) * b) by INT_1:def 10;

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

take c ; :: according to INT_1:def 5 :: thesis: b * c = (a mod b) - a

thus b * c = (a mod b) - a by A1; :: thesis: verum

assume b <> 0 ; :: thesis: a mod b,a are_congruent_mod b

then A1: a mod b = a - ((a div b) * b) by INT_1:def 10;

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

take c ; :: according to INT_1:def 5 :: thesis: b * c = (a mod b) - a

thus b * c = (a mod b) - a by A1; :: thesis: verum