for n being non zero Nat holds tau to_power n > tau_bar to_power n