for n being Nat st n <> 0 holds
tau_bar to_power n < 1 / 2