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