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

per cases ( (a + b) mod 4 = 2 or (a - b) mod 4 = 2 ) by SDM;

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

then not 4 divides a + b by INT162;
then 4 divides a - b by NEWTON03:73;
hence ( (a + b) mod 4 = 0 or (a - b) mod 4 = 0 ) by INT162; :: thesis: verum

end;

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

then not 4 divides a - b by INT162;
then 4 divides a + b by NEWTON03:73;
hence ( (a + b) mod 4 = 0 or (a - b) mod 4 = 0 ) by INT162; :: thesis: verum

end;

end;