defpred S_{1}[ Nat] means Fib ($1 + 1) >= Fib $1;

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

S_{1}[k + 1]
_{1}[ 0 ]
by PRE_FF:1;

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

A1: for k being Nat st S

S

proof

A2:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

Fib ((k + 1) + 1) = (Fib (k + 1)) + (Fib k) by PRE_FF:1;

then Fib ((k + 1) + 1) >= (Fib (k + 1)) + 0 by XREAL_1:6;

hence ( S_{1}[k] implies S_{1}[k + 1] )
; :: thesis: verum

end;Fib ((k + 1) + 1) = (Fib (k + 1)) + (Fib k) by PRE_FF:1;

then Fib ((k + 1) + 1) >= (Fib (k + 1)) + 0 by XREAL_1:6;

hence ( S

thus for k being Nat holds S