theorem :: NEWTON03:66

for m being non zero even Nat
for a, b being odd Nat st a <> b holds
2 |-count ((a |^ (2 * m)) - (b |^ (2 * m))) = (2 |-count ((a |^ m) - (b |^ m))) + 1