let m, n be non empty natural number ; :: thesis: ( m >= n implies Lucas m >= Lucas n )
assume pc: m >= n ; :: thesis: Lucas m >= Lucas n

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

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

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

end;

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

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

proof

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

proof

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

end;

B2: for k being non empty Nat st S₁[k] holds
S₁[k + 1]

proof

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

proof

let n be non empty Nat; :: thesis: Lucas (n + (k + 1)) >= Lucas n
reconsider p = n + k as Element of NAT by ORDINAL1:def 13;
p is non empty Element of NAT ;
then ( Lucas (n + k) >= Lucas n & Lucas ((n + k) + 1) >= Lucas (n + k) ) by B4, 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 empty Nat holds S₁[k] from NAT_1:sch 10(B1, B2);
hence for k, n being non empty Nat holds Lucas (n + k) >= Lucas n ; :: thesis: verum

end;

( k is non empty Nat & n is non empty Nat ) by A1, P0;
hence Lucas m >= Lucas n by A1, A3; :: thesis: verum

end;

end;