for n, m being Nat
for r being Real st m is odd & n >= m & r < 0 & r > - 1 holds
r to_power n >= r to_power m