let n be natural number ; :: thesis: ( n >= 2 implies Lucas n = [\((tau to_power n) + (1 / 2))/] )
assume B0: n >= 2 ; :: thesis: Lucas n = [\((tau to_power n) + (1 / 2))/]
then 1 / 2 >= tau_bar to_power n by hop8;
then (tau to_power n) + (1 / 2) >= (tau to_power n) + (tau_bar to_power n) by XREAL_1:8;
then B1: (tau to_power n) + (1 / 2) >= Lucas n by FIB_NUM3:21;
n > 1 by B0, XXREAL_0:2;
then (1 / 2) - 1 < tau_bar to_power n by hop9;
then (tau to_power n) + ((1 / 2) - 1) < (tau to_power n) + (tau_bar 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 B1, INT_1:def 4; :: thesis: verum