theorem :: FIB_NUM4:13

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