let m be non zero Element of NAT ; :: thesis: Lucas (m + 1) >= Lucas m
thus Lucas (m + 1) >= Lucas m :: thesis: verum

proof

defpred S₁[ Nat] means Lucas ($1 + 1) >= Lucas $1;
A1: for k being non zero Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be non zero Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
S₁[k] and
S₁[k + 1] ; :: thesis: S₁[k + 2]
(Lucas (k + 2)) + (Lucas (k + 1)) = Lucas (k + 3) by Th13;
hence S₁[k + 2] by NAT_1:12; :: thesis: verum

end;

A2: S₁[2] by Th14, Th15;
A3: S₁[1] by Th11, Th14;
for k being non zero Nat holds S₁[k] from FIB_NUM2:sch 1(A3, A2, A1);
hence Lucas (m + 1) >= Lucas m ; :: thesis: verum

end;