theorem :: NEWTON01:27

for a, b, n being Nat st b > 0 & a > b holds
( ((a |^ n) - (b |^ n)) * (a + b) = ((a |^ n) + (b |^ n)) * (a - b) iff n = 1 ) by Lm57d;