defpred S1[ Nat] means Fib ($1 + 1) >= $1;
(0 + 1) + 1 = 2 ;
then A1: S1[1] by PRE_FF:1;
A2: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A3: S1[k] and
A4: S1[k + 1] ; :: thesis: S1[k + 2]
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: S1[k + 2]
hence S1[k + 2] by Lm1, Lm2, PRE_FF:1; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: S1[k + 2]
then 1 <= k by NAT_1:14;
then A5: 1 + (k + 1) <= k + (k + 1) by XREAL_1:6;
A6: Fib ((k + 2) + 1) = (Fib ((k + 1) + 1)) + (Fib (k + 1)) by PRE_FF:1;
A7: k + (k + 1) <= (Fib (k + 1)) + (k + 1) by A3, XREAL_1:6;
(Fib (k + 1)) + (k + 1) <= (Fib ((k + 1) + 1)) + (Fib (k + 1)) by A4, XREAL_1:6;
then k + (k + 1) <= Fib ((k + 2) + 1) by A6, A7, XXREAL_0:2;
hence S1[k + 2] by A5, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A8: S1[ 0 ] ;
thus for k being Nat holds S1[k] from FIB_NUM:sch 1(A8, A1, A2); :: thesis: verum