theorem LTAUPOW: :: NTALGO_2:21

for n being Nat st 3 <= n holds
tau to_power (n - 2) < Fib n