for n being Nat st n > 2 holds
tau_bar to_power n >= - (1 / (sqrt 5))