let a, b, n be Nat; :: thesis: ( b > 0 & a > b & ((a |^ n) - (b |^ n)) * (a + b) = ((a |^ n) + (b |^ n)) * (a - b) implies n = 1 )
assume A0: ( b > 0 & a > b & ((a |^ n) - (b |^ n)) * (a + b) = ((a |^ n) + (b |^ n)) * (a - b) ) ; :: thesis: n = 1
A1: ( a |^ 0 = 1 & b |^ 0 = 1 ) by NEWTON:4;

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: n = 1

then 0 * (a + b) = 2 * (a - b) by A0, A1;
hence n = 1 by A0; :: thesis: verum

end;

suppose A20: n > 0 ; :: thesis: n = 1

then A20a: n >= 1 by NAT_1:14;
(a |^ (n + 1)) - (b |^ (n + 1)) <= ((a |^ n) + (b |^ n)) * (a - b) by A0, A20, Lm57;
then n <= 1 by A0, Lm56a;
hence n = 1 by A20a, XXREAL_0:1; :: thesis: verum

end;

end;