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;