for a, b, c being Real st 0 < a & a <= b & c >= 0 holds
a to_power c <= b to_power c by Lm6;