for a, b, c being Real st a <= b & c >= 1 holds
c to_power a <= c to_power b