let a, b be odd Nat; :: thesis: ( 4 divides a + b iff not 4 divides a - b )
( a + b is even & a - b is even ) ;
then ( 2 divides a + b & 2 divides a - b ) ;
then consider t, z being Integer such that
A3: ( a + b = 2 * t & a - b = 2 * z ) ;
A5: ( t is odd iff z is even )

proof

( a = t + z & b = t - z ) by A3;
hence ( t is odd iff z is even ) ; :: thesis: verum

end;

A6: 2 * (2 gcd z) = |.2.| * (2 gcd z)
.= (2 * 2) gcd (2 * z) by INT_6:16 ;
A7: ( 2 * 2 divides a + b implies not 2 * 2 divides a - b )

proof

assume 2 * 2 divides a + b ; :: thesis: not 2 * 2 divides a - b
then |.(2 * 2).| = (2 * 2) gcd (2 * t) by A3, Th3
.= |.2.| * (t gcd 2) by INT_6:16 ;
then (2 * 2) gcd (2 * z) <> |.4.| by A5, A6, Th3;
hence not 2 * 2 divides a - b by A3, Th3; :: thesis: verum

end;

( not 2 * 2 divides a + b implies 2 * 2 divides a - b )

proof

assume not 2 * 2 divides a + b ; :: thesis: 2 * 2 divides a - b
then not |.(2 * 2).| = (2 * 2) gcd (2 * t) by A3, Th3;
then not |.(2 * 2).| = |.2.| * (t gcd 2) by INT_6:16;
then (2 * 2) gcd (2 * z) = |.4.| by A5, A6, Th3;
hence 2 * 2 divides a - b by A3, Th3; :: thesis: verum

end;

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