let a, b, n be Nat; :: thesis: ( a <= b implies a |^ n <= b |^ n )

per cases ( n = 0 or 1 <= n ) by NAT_1:14;

suppose A1: n = 0 ; :: thesis: ( a <= b implies a |^ n <= b |^ n )

( a |^ 0 = 1 & b |^ 0 = 1 ) by NEWTON:4;
hence ( a <= b implies a |^ n <= b |^ n ) by A1; :: thesis: verum

end;

suppose A1: 1 <= n ; :: thesis: ( a <= b implies a |^ n <= b |^ n )

assume a <= b ; :: thesis: a |^ n <= b |^ n

per cases then ( a < b or a = b ) by XXREAL_0:1;

suppose a < b ; :: thesis: a |^ n <= b |^ n

hence a |^ n <= b |^ n by A1, PREPOWER:10; :: thesis: verum

end;

suppose a = b ; :: thesis: a |^ n <= b |^ n

hence a |^ n <= b |^ n ; :: thesis: verum

end;

end;

end;

end;