defpred S1[ Nat] means (Lucas $1) + (Fib $1) = 2 * (Fib ($1 + 1));
let n be Nat; :: thesis: (Lucas n) + (Fib n) = 2 * (Fib (n + 1))
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 that
A2: S1[k] and
A3: S1[k + 1] ; :: thesis: S1[k + 2]
(Lucas (k + 2)) + (Fib (k + 2)) = ((Lucas k) + (Lucas (k + 1))) + (Fib (k + 2)) by Th12
.= ((Lucas k) + (Lucas (k + 1))) + ((Fib k) + (Fib (k + 1))) by FIB_NUM2:24
.= (2 * (Fib (k + 1))) + (2 * (Fib ((k + 1) + 1))) by A2, A3
.= 2 * ((Fib (k + 1)) + (Fib (k + 2)))
.= 2 * (Fib (k + 3)) by FIB_NUM2:25
.= 2 * (Fib ((k + 2) + 1)) ;
hence S1[k + 2] ; :: thesis: verum
end;
(0 + 1) + 1 = 2 ;
then Fib 2 = 1 by PRE_FF:1;
then A4: S1[1] by Th11, PRE_FF:1;
A5: S1[ 0 ] by Th11, PRE_FF:1;
for k being Nat holds S1[k] from FIB_NUM:sch 1(A5, A4, A1);
 hence (Lucas n) + (Fib n) = 2 * (Fib (n + 1)) ; :: thesis: verum