theorem Even: :: NEWTON03:23
for m, n being Nat
for a, b being odd Nat st 2 |^ m divides (a |^ n) - (b |^ n) holds
2 |^ (m + 1) divides (a |^ (2 * n)) - (b |^ (2 * n))