let a be Integer; :: thesis: for b being even Integer st not b divides a & a mod b is odd holds
(- a) mod b is odd
let b be even Integer; :: thesis: ( not b divides a & a mod b is odd implies (- a) mod b is odd )
assume A1: not b divides a ; :: thesis: ( not a mod b is odd or (- a) mod b is odd )

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

suppose b is zero ; :: thesis: ( not a mod b is odd or (- a) mod b is odd )

hence ( not a mod b is odd or (- a) mod b is odd ) ; :: thesis: verum

end;

suppose not b is zero ; :: thesis: ( not a mod b is odd or (- a) mod b is odd )

then reconsider b = b as non zero Integer ;
(a mod b) + ((- a) mod b) is even by A1, MOD;
hence ( not a mod b is odd or (- a) mod b is odd ) ; :: thesis: verum

end;

end;