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

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

suppose b is zero ; :: thesis: ( (a mod b) + ((- a) mod b) = 0 or (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) = 0 or (a mod b) + ((- a) mod b) = b ) ; :: thesis: verum

end;

suppose not b is zero ; :: thesis: ( (a mod b) + ((- a) mod b) = 0 or (a mod b) + ((- a) mod b) = b )

then reconsider b = b as non zero Integer ;

per cases ( b divides a or not b divides a ) ;

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

then ( a mod b = 0 & (- a) mod b = 0 ) by INT162, INT_2:10;
hence ( (a mod b) + ((- a) mod b) = 0 or (a mod b) + ((- a) mod b) = b ) ; :: thesis: verum

end;

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

hence ( (a mod b) + ((- a) mod b) = 0 or (a mod b) + ((- a) mod b) = b ) by MOD; :: thesis: verum

end;

end;

end;

end;