theorem Th15: :: FIB_NUM4:15
for n being Nat st n > 2 holds
tau_bar to_power n >= - (1 / (sqrt 5))