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

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