for n being Nat st n > 1 holds
Fib n < Fib (n + 1)