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 S1[ Nat] means for n being non zero Nat holds Lucas (n + $1) >= Lucas n;
A5: S1[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 S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[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 S1[k + 1] ; :: thesis: verum
end;
for k being non zero Nat holds S1[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;