let n be Nat; :: thesis: for a, b being odd Nat st 4 divides a - b holds
not 4 divides (a |^ n) + (b |^ n)
let a, b be odd Nat; :: thesis: ( 4 divides a - b implies not 4 divides (a |^ n) + (b |^ n) )
assume A1: 4 divides a - b ; :: thesis: not 4 divides (a |^ n) + (b |^ n)

per cases ( n is odd or n is even ) ;

suppose n is odd ; :: thesis: not 4 divides (a |^ n) + (b |^ n)

hence not 4 divides (a |^ n) + (b |^ n) by A1, NEWTON02:69; :: thesis: verum

end;

suppose n is even ; :: thesis: not 4 divides (a |^ n) + (b |^ n)

then 4 divides (a |^ n) - (b |^ n) by NEWTON02:65;
hence not 4 divides (a |^ n) + (b |^ n) by NEWTON02:58; :: thesis: verum

end;

end;