theorem Th10: :: FIB_NUM4:10
for n, m being Nat st m is odd & n >= m holds
tau_bar to_power n >= tau_bar to_power m