let a, b, n be Nat; :: thesis: ( a |^ n > b |^ n implies a |^ (n + 1) > b |^ (n + 1) )
assume A1: a |^ n > b |^ n ; :: thesis: a |^ (n + 1) > b |^ (n + 1)
A2: ( a |^ (n + 1) = a * (a |^ n) & b |^ (n + 1) = b * (b |^ n) ) by NEWTON:6;
A3: a > b by A1, Lm3a;
then A4: a * (a |^ n) > a * (b |^ n) by A1, XREAL_1:68;
(b |^ n) * a >= (b |^ n) * b by A3, XREAL_1:66;
hence a |^ (n + 1) > b |^ (n + 1) by A2, A4, XXREAL_0:2; :: thesis: verum