let n be natural number ; :: thesis: ( n >= 2 implies Lucas n = [/((tau to_power n) - (1 / 2))\] )
assume A0: n >= 2 ; :: thesis: Lucas n = [/((tau to_power n) - (1 / 2))\]
then n > 1 by XXREAL_0:2;
then - (1 / 2) <= tau_bar to_power n by hop9;
then (- (1 / 2)) + (tau to_power n) <= (tau_bar to_power n) + (tau to_power n) by XREAL_1:8;
then A1: (tau to_power n) - (1 / 2) <= Lucas n by FIB_NUM3:21;
tau_bar to_power n < 1 / 2 by hop8, A0;
then (tau_bar to_power n) + (tau to_power n) < (1 / 2) + (tau to_power n) by XREAL_1:8;
then ((tau to_power n) - (1 / 2)) + 1 > Lucas n by FIB_NUM3:21;
hence Lucas n = [/((tau to_power n) - (1 / 2))\] by A1, INT_1:def 5; :: thesis: verum