defpred S1[ Nat] means Lucas ($1 + 1) = (Fib $1) + (Fib ($1 + 2));
A1: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume A2: ( S1[k] & S1[k + 1] ) ; :: thesis: S1[k + 2]
Fib ((k + 2) + 2) = Fib (((k + 2) + 1) + 1) ;
then A3: Fib ((k + 2) + 2) = (Fib (k + 2)) + (Fib ((k + 2) + 1)) by PRE_FF:1;
Lucas ((k + 2) + 1) = (Lucas (k + 1)) + (Lucas ((k + 1) + 1)) by Th11
.= (((Fib k) + (Fib (k + 1))) + (Fib (k + 2))) + (Fib ((k + 1) + 2)) by A2
.= ((Fib ((k + 1) + 1)) + (Fib (k + 2))) + (Fib ((k + 1) + 2)) by PRE_FF:1
.= (Fib (k + 2)) + (Fib ((k + 2) + 2)) by A3 ;
hence S1[k + 2] ; :: thesis: verum
end;
(0 + 1) + 1 = 2 ;
then Fib 2 = 1 by PRE_FF:1;
then A4: S1[1] by Th14, PRE_FF:1;
(0 + 1) + 1 = 2 ;
then A5: S1[ 0 ] by Th11, PRE_FF:1;
thus for k being Nat holds S1[k] from FIB_NUM:sch 1(A5, A4, A1); :: thesis: verum