let n, k be Nat; :: thesis: ( k > 1 & k < n implies Fib k < Fib n )
assume A1: k > 1 ; :: thesis: ( not k < n or Fib k < Fib n )
assume A2: k < n ; :: thesis: Fib k < Fib n
then consider m being Nat such that
A3: n = k + m by NAT_1:10;
reconsider k = k as non zero Element of NAT by A1, ORDINAL1:def 12;
reconsider m = m as non zero Element of NAT by A2, A3, ORDINAL1:def 12;
for k, m being non zero Element of NAT st k > 1 holds
Fib k < Fib (k + m)

proof

let k, m be non zero Element of NAT ; :: thesis: ( k > 1 implies Fib k < Fib (k + m) )
assume A4: k > 1 ; :: thesis: Fib k < Fib (k + m)
defpred S₁[ Nat] means Fib k < Fib (k + $1);
A5: for r being non zero Nat st S₁[r] holds
S₁[r + 1]

proof

let r be non zero Nat; :: thesis: ( S₁[r] implies S₁[r + 1] )
k + r > 0 + 1 by A4, XREAL_1:8;
then A6: Fib (k + r) < Fib ((k + r) + 1) by Th44;
assume S₁[r] ; :: thesis: S₁[r + 1]
hence S₁[r + 1] by A6, XXREAL_0:2; :: thesis: verum

end;

A7: S₁[1] by A4, Th44;
for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A7, A5);
hence Fib k < Fib (k + m) ; :: thesis: verum

end;

then Fib k < Fib (k + m) by A1;
hence Fib k < Fib n by A3; :: thesis: verum