defpred S₁[ Nat] means Lucas $1 >= $1;
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A3: S₁[k] and
A4: S₁[k + 1] ; :: thesis: S₁[k + 2]

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

suppose k = 0 ; :: thesis: S₁[k + 2]

hence S₁[k + 2] by Th14; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: S₁[k + 2]

then 1 <= k by NAT_1:14;
then A5: 1 + (k + 1) <= k + (k + 1) by XREAL_1:8;
A6: k + (k + 1) <= (Lucas k) + (k + 1) by A3, XREAL_1:8;
( Lucas ((k + 1) + 1) = (Lucas (k + 1)) + (Lucas k) & (Lucas k) + (k + 1) <= (Lucas (k + 1)) + (Lucas k) ) by A4, Th11, XREAL_1:8;
then k + (k + 1) <= Lucas ((k + 1) + 1) by A6, XXREAL_0:2;
hence S₁[k + 2] by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A7: S₁[1] by Th11;
thus for k being Nat holds S₁[k] from FIB_NUM:sch 1(A1, A7, A2); :: thesis: verum