let a, b be Integer; :: thesis: a mod b = b * (frac (a / b))

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

suppose b is zero ; :: thesis: a mod b = b * (frac (a / b))

hence a mod b = b * (frac (a / b)) ; :: thesis: verum

end;

suppose not b is zero ; :: thesis: a mod b = b * (frac (a / b))

then reconsider b = b as non zero Integer ;
a mod b = a - ((a div b) * b) by INT_1:def 10
.= a - ([\(a / b)/] * b) by INT_1:def 9
.= ((a / b) * b) - ([\(a / b)/] * b) by XCMPLX_1:87
.= ((a / b) - [\(a / b)/]) * b
.= b * (frac (a / b)) by INT_1:def 8 ;
hence a mod b = b * (frac (a / b)) ; :: thesis: verum

end;

end;