theorem Th16: :: FIB_NUM4:16

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