let n be Nat; :: thesis: for a, b being odd Nat st 4 divides a - b holds
4 divides (a |^ n) - (b |^ n)
let a, b be odd Nat; :: thesis: ( 4 divides a - b implies 4 divides (a |^ n) - (b |^ n) )
assume A1: 4 divides a - b ; :: thesis: 4 divides (a |^ n) - (b |^ n)
a - b divides (a |^ n) - (b |^ n) by NEWTON01:33;
hence 4 divides (a |^ n) - (b |^ n) by A1, INT_2:9; :: thesis: verum