defpred S_{1}[ Nat] means Fib ($1 + 1) >= $1;

(0 + 1) + 1 = 2 ;

then A1: S_{1}[1]
by PRE_FF:1;

A2: for k being Nat st S_{1}[k] & S_{1}[k + 1] holds

S_{1}[k + 2]
_{1}[ 0 ]
;

thus for k being Nat holds S_{1}[k]
from FIB_NUM:sch 1(A8, A1, A2); :: thesis: verum

(0 + 1) + 1 = 2 ;

then A1: S

A2: for k being Nat st S

S

proof

A8:
S
let k be Nat; :: thesis: ( S_{1}[k] & S_{1}[k + 1] implies S_{1}[k + 2] )

assume that

A3: S_{1}[k]
and

A4: S_{1}[k + 1]
; :: thesis: S_{1}[k + 2]

end;assume that

A3: S

A4: S

per cases
( k = 0 or k <> 0 )
;

end;

suppose
k <> 0
; :: thesis: S_{1}[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 S_{1}[k + 2]
by A5, XXREAL_0:2; :: thesis: verum

end;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 S

thus for k being Nat holds S