let m, n be non zero Nat; :: thesis: ( m >= n implies Lucas m >= Lucas n )
assume A1: m >= n ; :: thesis: Lucas m >= Lucas n

per cases ( m = n or m > n ) by A1, XXREAL_0:1;

suppose m = n ; :: thesis: Lucas m >= Lucas n

hence Lucas m >= Lucas n ; :: thesis: verum

end;

suppose A2: m > n ; :: thesis: Lucas m >= Lucas n

then consider k being Nat such that
A3: m = n + k by NAT_1:10;
A4: for k, n being non zero Nat holds Lucas (n + k) >= Lucas n

proof

defpred S₁[ Nat] means for n being non zero Nat holds Lucas (n + $1) >= Lucas n;
A5: S₁[1]

proof

let n be non zero Nat; :: thesis: Lucas (n + 1) >= Lucas n
( n - 0 is Element of NAT & n + 1 is Element of NAT ) by ORDINAL1:def 12;
hence Lucas (n + 1) >= Lucas n by FIB_NUM3:18; :: thesis: verum

end;

A6: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
for n being non zero Nat holds Lucas (n + (k + 1)) >= Lucas n

proof

let n be non zero Nat; :: thesis: Lucas (n + (k + 1)) >= Lucas n
reconsider p = n + k as Element of NAT by ORDINAL1:def 12;
p is non zero Element of NAT ;
then ( Lucas (n + k) >= Lucas n & Lucas ((n + k) + 1) >= Lucas (n + k) ) by A7, FIB_NUM3:18;
hence Lucas (n + (k + 1)) >= Lucas n by XXREAL_0:2; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A5, A6);
hence for k, n being non zero Nat holds Lucas (n + k) >= Lucas n ; :: thesis: verum

end;

( k is non zero Nat & n is non zero Nat ) by A3, A2;
hence Lucas m >= Lucas n by A3, A4; :: thesis: verum

end;

end;