for n being Nat holds Fib n <= Fib (n + 1)