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 S1[ Nat] means Fib k < Fib (k + $1);
A5: for r being non zero Nat st S1[r] holds
S1[r + 1]
proof
let r be non zero Nat; :: thesis: ( S1[r] implies S1[r + 1] )
k + r > 0 + 1 by A4, XREAL_1:8;
then A6: Fib (k + r) < Fib ((k + r) + 1) by Th44;
assume S1[r] ; :: thesis: S1[r + 1]
hence S1[r + 1] by A6, XXREAL_0:2; :: thesis: verum
end;
A7: S1[1] by A4, Th44;
for k being non zero Nat holds S1[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