let a, b be non zero Integer; :: thesis: ( not b mod a = (- b) mod a or a is even or a divides b )
assume A1: b mod a = (- b) mod a ; :: thesis: ( a is even or a divides b )
assume ( not a is even & not a divides b ) ; :: thesis: contradiction
then ( b mod a is odd iff (- b) mod a is even ) by MOO;
hence contradiction by A1; :: thesis: verum