defpred S₁[ Nat] means Lucas $1 >= $1;
A1: S₁[ 0 ] ;
A2: S₁[1] by Th11;
A3: 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
A4: S₁[k] and
A5: 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 A6: 1 <= k by NAT_1:14;
A7: Lucas ((k + 1) + 1) = (Lucas (k + 1)) + (Lucas k) by Th11;
A8: (Lucas k) + (k + 1) <= (Lucas (k + 1)) + (Lucas k) by A5, XREAL_1:8;
k + (k + 1) <= (Lucas k) + (k + 1) by A4, XREAL_1:8;
then A9: k + (k + 1) <= Lucas ((k + 1) + 1) by A7, A8, XXREAL_0:2;
1 + (k + 1) <= k + (k + 1) by A6, XREAL_1:8;
hence S₁[k + 2] by A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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