defpred S₁[ Nat] means (tau to_power $1) + (tau to_power ($1 + 1)) = tau to_power ($1 + 2);
let n be Nat; :: thesis: (tau to_power n) + (tau to_power (n + 1)) = tau to_power (n + 2)
A1: (tau to_power 0) + (tau to_power (0 + 1)) = 1 + (tau to_power 1) by POWER:24
.= 1 + ((1 + (sqrt 5)) / 2) by FIB_NUM:def 1, POWER:25
.= (((1 + (sqrt 5)) + (sqrt 5)) + 5) / 4
.= (((1 + (sqrt 5)) + (sqrt 5)) + (sqrt (5 ^2))) / 4 by SQUARE_1:22
.= (((1 + (1 * (sqrt 5))) + ((sqrt 5) * 1)) + ((sqrt 5) * (sqrt 5))) / 4 by SQUARE_1:29
.= tau * tau by FIB_NUM:def 1
.= (tau to_power 1) * tau by POWER:25
.= (tau to_power 1) * (tau to_power 1) by POWER:25
.= tau to_power (1 + 1) by POWER:27
.= tau to_power (0 + 2) ;
A2: 1 + tau = 1 + (tau to_power 1) by POWER:25
.= tau to_power (0 + 2) by A1, POWER:24 ;
A3: for k being Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
S₁[k] and
S₁[k + 1] ; :: thesis: S₁[k + 2]
(tau to_power (k + 2)) + (tau to_power ((k + 2) + 1)) = (tau to_power (k + 2)) + ((tau to_power (k + 2)) * (tau to_power 1)) by POWER:27
.= (tau to_power (k + 2)) * (1 + (tau to_power 1))
.= (tau to_power (k + 2)) * (tau to_power 2) by A2, POWER:25
.= tau to_power ((k + 2) + 2) by POWER:27 ;
hence S₁[k + 2] ; :: thesis: verum

end;

(tau to_power 1) + (tau to_power (1 + 1)) = tau + (tau to_power (1 + 1)) by POWER:25
.= tau + ((tau to_power 1) * (tau to_power 1)) by POWER:27
.= tau + ((tau to_power 1) * tau) by POWER:25
.= tau + (tau * tau) by POWER:25
.= tau * (1 + tau)
.= (tau to_power 1) * (tau to_power 2) by A2, POWER:25
.= tau to_power (1 + 2) by POWER:27 ;
then A4: S₁[1] ;
A5: S₁[ 0 ] by A1;
for k being Nat holds S₁[k] from FIB_NUM:sch 1(A5, A4, A3);
hence (tau to_power n) + (tau to_power (n + 1)) = tau to_power (n + 2) ; :: thesis: verum