let n be Nat; :: thesis: ( n >= 2 implies Lucas n = [\((tau to_power n) + (1 / 2))/] )
assume A1: n >= 2 ; :: thesis: Lucas n = [\((tau to_power n) + (1 / 2))/]
then 1 / 2 >= tau_bar to_power n by Th8;
then (tau to_power n) + (1 / 2) >= (tau to_power n) + (tau_bar to_power n) by XREAL_1:6;
then A2: (tau to_power n) + (1 / 2) >= Lucas n by FIB_NUM3:21;
n > 1 by A1, XXREAL_0:2;
then (1 / 2) - 1 < tau_bar to_power n by Th14;
then (tau to_power n) + ((1 / 2) - 1) < (tau to_power n) + (tau_bar to_power n) by XREAL_1:6;
then ((tau to_power n) + (1 / 2)) - 1 < Lucas n by FIB_NUM3:21;
hence Lucas n = [\((tau to_power n) + (1 / 2))/] by A2, INT_1:def 6; :: thesis: verum