let a, b, c be Integer; :: thesis: a mod b = ((b * c) + a) mod b

per cases ( b is zero or not b is zero ) ;

suppose b is zero ; :: thesis: a mod b = ((b * c) + a) mod b

hence a mod b = ((b * c) + a) mod b ; :: thesis: verum

end;

suppose not b is zero ; :: thesis: a mod b = ((b * c) + a) mod b

then reconsider b = b as non zero Integer ;
a mod b = a - (b * (a div b)) by INT_1:def 10
.= (a + (b * c)) - (b * ((a div b) + c))
.= (a + (b * c)) - (b * ((a + (b * c)) div b)) by NAT_D:61
.= (a + (b * c)) mod b by INT_1:def 10 ;
hence a mod b = ((b * c) + a) mod b ; :: thesis: verum

end;

end;