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