for n, m being Nat st n is even & m is even & n >= m holds
tau_bar to_power n <= tau_bar to_power m