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