let a, b be Integer; :: thesis: ( not b divides a implies (a mod b) + ((- a) mod b) = b )
assume A1: not b divides a ; :: thesis: (a mod b) + ((- a) mod b) = b
then reconsider a = a as non zero Integer by INT_2:12;

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

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

then reconsider b = b as zero Integer ;
( a mod b = 0 & (- a) mod b = 0 ) ;
hence (a mod b) + ((- a) mod b) = b ; :: thesis: verum

end;

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

then reconsider b = b as non zero Integer ;
reconsider r = a / b as non integer Real by A1, NUMBER13:4;
( a mod b = b * (frac (a / b)) & (- a) mod b = b * (frac ((- a) / b)) ) by REAL_3:6;
then (a mod b) + ((- a) mod b) = (b * (frac (a / b))) + (b * (frac (- (a / b))))
.= b * ((frac r) + (frac (- r)))
.= b * 1 by FAA ;
hence (a mod b) + ((- a) mod b) = b ; :: thesis: verum

end;

end;