for a, b being non negative Real
for c being positive Real holds
( a >= b iff a to_power c >= b to_power c )