let n, r be non empty Element of NAT ; :: thesis: ( r <= n implies ((Fib n) ^2 ) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2 ) )
assume A1: r <= n ; :: thesis: ((Fib n) ^2 ) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2 )
set S = 1 / (sqrt 5);
set X = n + r;
set Y = n -' r;
set T = tau ;
A2: - tau <> 0 by Th35;
reconsider T = tau as non empty real number by Th35;
set tn = T to_power n;
set tx = T to_power (n + r);
set ty = T to_power (n -' r);
set tnu = T to_power (- n);
set txu = T to_power (- (n + r));
set tyu = T to_power (- (n -' r));
A3: (n + r) + (n -' r) = (r + n) + (n - r) by A1, XREAL_1:235
.= ((r + n) + n) - r
.= (r + (2 * n)) -' r by NAT_1:12, XREAL_1:235
.= (r -' r) + (2 * n) by NAT_D:38
.= 0 + (2 * n) by XREAL_1:234
.= 2 * n ;
A4: (n + r) - (n -' r) = (n + r) - (n - r) by A1, XREAL_1:235
.= 2 * r ;
A5: not - 1 is empty ;
A6: - 1 = (2 * (- 1)) + 1 ;
((Fib n) ^2 ) - ((Fib (n + r)) * (Fib (n -' r))) = ((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2 ) - ((Fib (n + r)) * (Fib (n -' r))) by FIB_NUM:7
.= ((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2 ) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (Fib (n -' r))) by FIB_NUM:7
.= ((((T to_power n) - (tau_bar to_power n)) / (sqrt 5)) ^2 ) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5))) by FIB_NUM:7
.= ((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2 ) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) / (sqrt 5)) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5))) by XCMPLX_1:100
.= ((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2 ) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) * (1 / (sqrt 5))) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) / (sqrt 5))) by XCMPLX_1:100
.= ((((T to_power n) - (tau_bar to_power n)) * (1 / (sqrt 5))) ^2 ) - ((((T to_power (n + r)) - (tau_bar to_power (n + r))) * (1 / (sqrt 5))) * (((T to_power (n -' r)) - (tau_bar to_power (n -' r))) * (1 / (sqrt 5)))) by XCMPLX_1:100
.= ((1 / (sqrt 5)) ^2 ) * (((((T to_power n) ^2 ) - ((2 * (T to_power n)) * (((- T) to_power (- 1)) to_power n))) + ((((- T) to_power (- 1)) to_power n) ^2 )) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r))))) by Th36
.= ((1 / (sqrt 5)) ^2 ) * (((((T to_power n) ^2 ) - ((2 * (T to_power n)) * ((- T) to_power ((- 1) * n)))) + ((((- T) to_power (- 1)) to_power n) ^2 )) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r))))) by A2, A6, Th8
.= ((1 / (sqrt 5)) ^2 ) * (((((T to_power n) ^2 ) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power ((- 1) * n)) ^2 )) - (((T to_power (n + r)) - (((- T) to_power (- 1)) to_power (n + r))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r))))) by A2, A6, Th8
.= ((1 / (sqrt 5)) ^2 ) * (((((T to_power n) ^2 ) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power (- n)) ^2 )) - (((T to_power (n + r)) - ((- T) to_power ((- 1) * (n + r)))) * ((T to_power (n -' r)) - (((- T) to_power (- 1)) to_power (n -' r))))) by Th37
.= ((1 / (sqrt 5)) ^2 ) * (((((T to_power n) ^2 ) - ((2 * (T to_power n)) * ((- T) to_power (- n)))) + (((- T) to_power (- n)) ^2 )) - (((T to_power (n + r)) - ((- T) to_power (- (n + r)))) * ((T to_power (n -' r)) - ((- T) to_power ((- 1) * (n -' r)))))) by Th37
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * (T to_power n)) * (((- 1) * T) to_power (- n)))) + ((((- 1) * T) to_power (- n)) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) * T) to_power (- (n -' r)))))
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * (T to_power n)) * (((- 1) * T) to_power (- n)))) + ((((- 1) * T) to_power (- n)) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th6
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) * T) to_power (- n)) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th6
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) * T) to_power (- (n -' r))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th6
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) * T) to_power (- (n + r))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th6
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - ((((- 1) * T) to_power (- (n + r))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th6
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * (T to_power n)) * (((- 1) to_power (- n)) * (T to_power (- n))))) + ((((- 1) to_power (- n)) * (T to_power (- n))) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power (n + r)) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (((- 1) to_power (- (n -' r))) * (T to_power (- (n -' r)))))) by Th6
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * ((T to_power n) * (T to_power (- n)))) * ((- 1) to_power (- n)))) + ((((- 1) to_power (- n)) ^2 ) * ((T to_power (- n)) ^2 ))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r)))))
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - ((2 * 1) * ((- 1) to_power (- n)))) + ((((- 1) to_power (- n)) ^2 ) * ((T to_power (- n)) ^2 ))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n -' r))))) by Th12
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + (1 * ((T to_power (- n)) ^2 ))) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * (T to_power (- (n -' r)))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r))))) by Th9
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) * (1 / (T to_power (n -' r)))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r))))) by Th35, POWER:33
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + (((T to_power (n + r)) / (T to_power (n -' r))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r))))) by XCMPLX_1:100
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - ((T to_power (n + r)) * (T to_power (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + ((((- 1) to_power (- (n + r))) * (T to_power (- (n + r)))) * (T to_power (n -' r)))) - (((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * (T to_power (- (n + r)))) * (T to_power (- (n -' r))))) by Th35, POWER:34
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) * (T to_power (- (n + r)))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by Th35, POWER:32
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) * (1 / (T to_power (n + r)))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by Th35, POWER:33
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * ((T to_power (n -' r)) / (T to_power (n + r))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by XCMPLX_1:100
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power ((n -' r) - (n + r))))) - ((((- 1) to_power (- (n + r))) * ((- 1) to_power (- (n -' r)))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by Th35, POWER:34
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power ((n + r) + (n -' r)))) + ((T to_power ((n + r) - (n -' r))) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power ((n -' r) - (n + r))))) - (((- 1) to_power ((- (n + r)) - (n -' r))) * ((T to_power (- (n + r))) * (T to_power (- (n -' r)))))) by A5, Th10
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (((- 1) to_power (- (2 * n))) * (T to_power (- (2 * n))))) by A3, Th10
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) ^2 ) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (1 * (T to_power (- (2 * n))))) by Th11
.= ((1 / (sqrt 5)) ^2 ) * ((((((((T to_power n) to_power 2) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (1 * (T to_power (- (2 * n))))) by POWER:53
.= ((1 / (sqrt 5)) ^2 ) * (((((((T to_power (2 * n)) - (2 * ((- 1) to_power (- n)))) + ((T to_power (- n)) ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n)))) by Th35, POWER:38
.= ((1 / (sqrt 5)) ^2 ) * (((((((T to_power (2 * n)) - (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2 )) - (T to_power (2 * n))) + ((T to_power (2 * r)) * ((- 1) to_power (- (n -' r))))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n)))) by Th13
.= ((1 / (sqrt 5)) ^2 ) * (((((((T to_power (2 * n)) - (T to_power (2 * n))) - (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2 )) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (- (n + r))) * (T to_power (- (2 * r))))) - (T to_power (- (2 * n)))) by Th13
.= ((1 / (sqrt 5)) ^2 ) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2 )) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) - (T to_power (2 * (- n)))) by Th13
.= ((1 / (sqrt 5)) ^2 ) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (- n)) ^2 )) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) - ((T to_power (- n)) to_power 2)) by Th35, POWER:38
.= ((1 / (sqrt 5)) ^2 ) * (((((- (2 * ((- 1) to_power n))) + ((T to_power (2 * r)) * ((- 1) to_power (n -' r)))) + (((- 1) to_power (n + r)) * (T to_power (- (2 * r))))) + ((T to_power (- n)) ^2 )) - ((T to_power (- n)) ^2 )) by POWER:53
.= ((1 / (sqrt 5)) ^2 ) * (((- (2 * ((- 1) to_power ((n -' r) + r)))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + (((- 1) to_power ((2 * r) + (n -' r))) * (T to_power (- (2 * r))))) by A4
.= ((1 / (sqrt 5)) ^2 ) * (((- (2 * (((- 1) to_power r) * ((- 1) to_power (n -' r))))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + (((- 1) to_power ((2 * r) + (n -' r))) * (T to_power (- (2 * r))))) by Th7
.= ((1 / (sqrt 5)) ^2 ) * (((- (2 * (((- 1) to_power r) * ((- 1) to_power (n -' r))))) + (((- 1) to_power (n -' r)) * (T to_power (2 * r)))) + ((((- 1) to_power (2 * r)) * ((- 1) to_power (n -' r))) * (T to_power (- (2 * r))))) by Th7
.= (((1 / (sqrt 5)) ^2 ) * (((- (2 * ((- 1) to_power r))) + (T to_power (2 * r))) + ((T to_power (- (2 * r))) * ((- 1) to_power (2 * r))))) * ((- 1) to_power (n -' r))
.= (((1 / (sqrt 5)) ^2 ) * (((- (2 * ((- 1) to_power r))) + (T to_power (2 * r))) + ((T to_power (- (2 * r))) * 1))) * ((- 1) to_power (n -' r)) by Th5
.= (((1 / (sqrt 5)) ^2 ) * (((T to_power (2 * r)) - (2 * ((- 1) to_power r))) + (T to_power (2 * (- r))))) * ((- 1) to_power (n -' r))
.= (((1 / (sqrt 5)) ^2 ) * ((((T to_power r) to_power 2) - (2 * ((- 1) to_power r))) + (T to_power ((- r) * 2)))) * ((- 1) to_power (n -' r)) by Th35, POWER:38
.= (((1 / (sqrt 5)) ^2 ) * ((((T to_power r) ^2 ) - (2 * ((- 1) to_power r))) + (T to_power ((- r) * 2)))) * ((- 1) to_power (n -' r)) by POWER:53
.= ((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2 ) * ((((T to_power r) ^2 ) - (2 * ((- 1) to_power r))) + ((T to_power (- r)) to_power 2))) by Th35, POWER:38
.= ((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2 ) * ((((T to_power r) ^2 ) - (2 * ((- 1) to_power r))) + ((T to_power (- r)) ^2 ))) by POWER:53
.= ((- 1) to_power (n -' r)) * (((1 / (sqrt 5)) ^2 ) * (((tau to_power r) - (tau_bar to_power r)) ^2 )) by Th39
.= ((- 1) to_power (n -' r)) * ((((tau to_power r) - (tau_bar to_power r)) * (1 / (sqrt 5))) ^2 )
.= ((- 1) to_power (n -' r)) * ((((tau to_power r) - (tau_bar to_power r)) / (sqrt 5)) ^2 ) by XCMPLX_1:100
.= ((- 1) |^ (n -' r)) * ((((T to_power r) - (tau_bar to_power r)) / (sqrt 5)) ^2 ) by POWER:46
.= ((- 1) |^ (n -' r)) * ((Fib r) ^2 ) by FIB_NUM:7 ;
hence ((Fib n) ^2 ) - ((Fib (n + r)) * (Fib (n -' r))) = ((- 1) |^ (n -' r)) * ((Fib r) ^2 ) ; :: thesis: verum