let a, b be Integer; :: thesis: ( a mod (- b) = - ((- a) mod b) & (- a) mod b = - (a mod (- b)) )
( (- a) mod b = - ((- (- a)) mod (- b)) & a mod (- b) = - ((- a) mod (- (- b))) ) by MOD1;
hence ( a mod (- b) = - ((- a) mod b) & (- a) mod b = - (a mod (- b)) ) ; :: thesis: verum