let k be positive Real; :: thesis: for n being non positive Real holds (k + 1) to_power n < (k to_power n) + 1
let n be non positive Real; :: thesis: (k + 1) to_power n < (k to_power n) + 1

per cases ( n = 0 or n < 0 ) ;

suppose n = 0 ; :: thesis: (k + 1) to_power n < (k to_power n) + 1

then ( (k + 1) to_power n = 1 & k to_power n = 1 ) by POWER:24;
hence (k + 1) to_power n < (k to_power n) + 1 ; :: thesis: verum

end;

suppose n < 0 ; :: thesis: (k + 1) to_power n < (k to_power n) + 1

then reconsider n = n as negative Real ;
( (k + 1) to_power n is light & (k + 1) to_power n is positive ) ;
then ( ((k + 1) to_power n) + 0 < ((k + 1) to_power n) + (k to_power n) & ((k + 1) to_power n) + (k to_power n) < 1 + (k to_power n) ) by XREAL_1:6;
hence (k + 1) to_power n < (k to_power n) + 1 by XXREAL_0:2; :: thesis: verum

end;

end;