A1:
for k, n being Element of NAT holds Fib (n + k) >= Fib n

assume m >= n ; :: thesis: Fib m >= Fib n

then consider k being Nat such that

A6: m = n + k by NAT_1:10;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

m = n + k by A6;

hence Fib m >= Fib n by A1; :: thesis: verum

proof

let m, n be Element of NAT ; :: thesis: ( m >= n implies Fib m >= Fib n )
defpred S_{1}[ Nat] means for n being Element of NAT holds Fib (n + $1) >= Fib n;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A5: S_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A5, A2);

hence Fib (n + k) >= Fib n ; :: thesis: verum

end;A2: for k being Nat st S

S

proof

let k, n be Element of NAT ; :: thesis: Fib (n + k) >= Fib n
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let n be Element of NAT ; :: thesis: Fib (n + (k + 1)) >= Fib n

n + (k + 1) = (n + k) + 1 ;

then A4: Fib (n + (k + 1)) >= Fib (n + k) by Lm4;

Fib (n + k) >= Fib n by A3;

hence Fib (n + (k + 1)) >= Fib n by A4, XXREAL_0:2; :: thesis: verum

end;assume A3: S

let n be Element of NAT ; :: thesis: Fib (n + (k + 1)) >= Fib n

n + (k + 1) = (n + k) + 1 ;

then A4: Fib (n + (k + 1)) >= Fib (n + k) by Lm4;

Fib (n + k) >= Fib n by A3;

hence Fib (n + (k + 1)) >= Fib n by A4, XXREAL_0:2; :: thesis: verum

A5: S

for k being Nat holds S

hence Fib (n + k) >= Fib n ; :: thesis: verum

assume m >= n ; :: thesis: Fib m >= Fib n

then consider k being Nat such that

A6: m = n + k by NAT_1:10;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

m = n + k by A6;

hence Fib m >= Fib n by A1; :: thesis: verum