for n being Nat holds Fib n = (Fib (n + 2)) - (Fib (n + 1))