defpred S_{1}[ Nat] means Lucas $1 >= $1;

A1: S_{1}[ 0 ]
;

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

S_{1}[k + 2]
_{1}[1]
by Th11;

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

A1: S

A2: for k being Nat st S

S

proof

A7:
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: k + (k + 1) <= (Lucas k) + (k + 1) by A3, XREAL_1:6;

( Lucas ((k + 1) + 1) = (Lucas (k + 1)) + (Lucas k) & (Lucas k) + (k + 1) <= (Lucas (k + 1)) + (Lucas k) ) by A4, Th11, XREAL_1:6;

then k + (k + 1) <= Lucas ((k + 1) + 1) by A6, 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: k + (k + 1) <= (Lucas k) + (k + 1) by A3, XREAL_1:6;

( Lucas ((k + 1) + 1) = (Lucas (k + 1)) + (Lucas k) & (Lucas k) + (k + 1) <= (Lucas (k + 1)) + (Lucas k) ) by A4, Th11, XREAL_1:6;

then k + (k + 1) <= Lucas ((k + 1) + 1) by A6, XXREAL_0:2;

hence S

thus for k being Nat holds S