let k, m be Nat; :: thesis: ( Fib k < Fib (m + 1) & 1 < k implies Fib k <= Fib m )
assume that
A1: Fib k < Fib (m + 1) and
A0: 1 < k ; :: thesis: Fib k <= Fib m
k < m + 1 by A1, FIB_NUM2:45;
then k <= m by NAT_1:13;

per cases then ( k = m or k < m ) by XXREAL_0:1;

suppose k = m ; :: thesis: Fib k <= Fib m

hence Fib k <= Fib m ; :: thesis: verum

end;

suppose k < m ; :: thesis: Fib k <= Fib m

hence Fib k <= Fib m by A0, FIB_NUM2:46; :: thesis: verum

end;

end;