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