let L be Real; :: thesis: ( 0 < L & L < 1 implies for n, m being Nat st n <= m holds
L to_power m <= L to_power n )
assume A1: ( 0 < L & L < 1 ) ; :: thesis: for n, m being Nat st n <= m holds
L to_power m <= L to_power n
let n, m be Nat; :: thesis: ( n <= m implies L to_power m <= L to_power n )
assume A2: n <= m ; :: thesis: L to_power m <= L to_power n

per cases ( n < m or n = m ) by A2, XXREAL_0:1;

suppose n < m ; :: thesis: L to_power m <= L to_power n

hence L to_power m <= L to_power n by A1, POWER:40; :: thesis: verum

end;

suppose n = m ; :: thesis: L to_power m <= L to_power n

hence L to_power m <= L to_power n ; :: thesis: verum

end;

end;