let a, b be Integer; :: thesis: a mod b = - ((- a) mod (- b))

per cases ( b = 0 or b <> 0 ) ;

suppose A1: b = 0 ; :: thesis: a mod b = - ((- a) mod (- b))

then a mod b = 0
.= - ((- a) mod (- b)) by A1 ;
hence a mod b = - ((- a) mod (- b)) ; :: thesis: verum

end;

suppose A1: b <> 0 ; :: thesis: a mod b = - ((- a) mod (- b))

then a mod b = a - ((a div b) * b) by INT_1:def 10
.= a - ([\(a / b)/] * b) by INT_1:def 9
.= (- (- a)) + ([\(a / b)/] * (- b))
.= (- (- a)) + ([\((- a) / (- b))/] * (- b)) by XCMPLX_1:191
.= (- (- a)) + (((- a) div (- b)) * (- b)) by INT_1:def 9
.= - ((- a) - (((- a) div (- b)) * (- b)))
.= - ((- a) mod (- b)) by INT_1:def 10, A1 ;
hence a mod b = - ((- a) mod (- b)) ; :: thesis: verum

end;

end;