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