theorem :: NEWTON01:36
for a, b, m being Nat holds a + b divides (a |^ (2 * m)) - (b |^ (2 * m))