theorem :: FIB_NUM4:20

for n being Nat st n <> 0 holds
[\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n)