let a, b, c be real number ; :: thesis: ( a <= b & c > 1 implies c to_power a <= c to_power b )
assume a <= b ; :: thesis: ( not c > 1 or c to_power a <= c to_power b )
then ( a < b or a = b ) by XXREAL_0:1;
hence ( not c > 1 or c to_power a <= c to_power b ) by POWER:44; :: thesis: verum