defpred S₁[ Nat] means (tau_bar to_power $1) + (tau_bar to_power ($1 + 1)) = tau_bar to_power ($1 + 2);
let n be Nat; :: thesis: (tau_bar to_power n) + (tau_bar to_power (n + 1)) = tau_bar to_power (n + 2)
A1: (tau_bar to_power 0) + (tau_bar to_power (0 + 1)) = 1 + (tau_bar to_power 1) by POWER:24
.= 1 + ((1 - (sqrt 5)) / 2) by FIB_NUM:def 2, 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_bar * tau_bar by FIB_NUM:def 2
.= (tau_bar to_power 1) * tau_bar by POWER:25
.= (tau_bar to_power 1) * (tau_bar to_power 1) by POWER:25
.= tau_bar to_power (1 + 1) by FIB_NUM2:5
.= tau_bar to_power (0 + 2) ;
A2: tau_bar + 1 = tau_bar + (tau_bar to_power 0) by POWER:24
.= tau_bar to_power 2 by A1, POWER:25 ;
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_bar to_power (k + 2)) + (tau_bar to_power ((k + 2) + 1)) = (tau_bar to_power (k + 2)) + ((tau_bar to_power (k + 2)) * (tau_bar to_power 1)) by FIB_NUM2:5
.= (tau_bar to_power (k + 2)) * (1 + (tau_bar to_power 1))
.= (tau_bar to_power (k + 2)) * (tau_bar to_power 2) by A2, POWER:25
.= tau_bar to_power ((k + 2) + 2) by FIB_NUM2:5 ;
hence S₁[k + 2] ; :: thesis: verum

end;

(tau_bar to_power 1) + (tau_bar to_power (1 + 1)) = tau_bar + (tau_bar to_power (1 + 1)) by POWER:25
.= tau_bar + ((tau_bar to_power 1) * (tau_bar to_power 1)) by FIB_NUM2:5
.= tau_bar + ((tau_bar to_power 1) * tau_bar) by POWER:25
.= tau_bar + (tau_bar * tau_bar) by POWER:25
.= tau_bar * (1 + tau_bar)
.= (tau_bar to_power 1) * (tau_bar to_power 2) by A2, POWER:25
.= tau_bar to_power (1 + 2) by FIB_NUM2:5 ;
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_bar to_power n) + (tau_bar to_power (n + 1)) = tau_bar to_power (n + 2) ; :: thesis: verum