for a, b being odd Nat
for m being even Nat holds 2 |-count ((a |^ m) + (b |^ m)) = 1