for a, b being Nat
for n being odd Nat holds
( 3 divides (a |^ n) + (b |^ n) iff 3 divides a + b )