let k, n be Nat; :: thesis: ( k <> 1 & k < n implies Fib k < Fib n )
assume A1: ( k <> 1 & k < n ) ; :: thesis: Fib k < Fib n

per cases then ( k > 1 or k = 0 ) by NAT_1:25;

suppose k > 1 ; :: thesis: Fib k < Fib n

hence Fib k < Fib n by A1, FIB_NUM2:46; :: thesis: verum

end;

suppose k = 0 ; :: thesis: Fib k < Fib n

hence Fib k < Fib n by A1, LemmaFib0, PRE_FF:1; :: thesis: verum

end;

end;