let a, b be odd Integer; :: thesis: ( 4 divides a - b iff not 4 divides a + b )
reconsider t = |.a.| as odd Nat ;
reconsider u = |.b.| as odd Nat ;
A0: ( 4 divides t - u iff not 4 divides t + u ) by NEWTON02:58;
( 4 divides u - t iff not 4 divides u + t ) by NEWTON02:58;
then A0a: ( 4 divides u - t iff not 4 divides - (u + t) ) by INT_2:10;

per cases ( |.a.| = a or |.a.| = - a ) by ABSVALUE:1;

suppose A1: |.a.| = a ; :: thesis: ( 4 divides a - b iff not 4 divides a + b )

then reconsider a = a as Nat ;

per cases ( |.b.| = b or |.b.| = - b ) by ABSVALUE:1;

suppose |.b.| = b ; :: thesis: ( 4 divides a - b iff not 4 divides a + b )

hence ( 4 divides a - b iff not 4 divides a + b ) by NEWTON02:58, A1; :: thesis: verum

end;

suppose |.b.| = - b ; :: thesis: ( 4 divides a - b iff not 4 divides a + b )

hence ( 4 divides a - b iff not 4 divides a + b ) by A0, A1; :: thesis: verum

end;

end;

end;

suppose A1: |.a.| = - a ; :: thesis: ( 4 divides a - b iff not 4 divides a + b )

per cases ( |.b.| = b or |.b.| = - b ) by ABSVALUE:1;

suppose |.b.| = b ; :: thesis: ( 4 divides a - b iff not 4 divides a + b )

hence ( 4 divides a - b iff not 4 divides a + b ) by A0a, A1; :: thesis: verum

end;

suppose |.b.| = - b ; :: thesis: ( 4 divides a - b iff not 4 divides a + b )

hence ( 4 divides a - b iff not 4 divides a + b ) by A0a, A1; :: thesis: verum

end;

end;

end;

end;