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 n > 1 by XXREAL_0:2;
then - (1 / 2) <= tau_bar to_power n by Th14;
then (- (1 / 2)) + (tau to_power n) <= (tau_bar to_power n) + (tau to_power n) by XREAL_1:6;
then A2: (tau to_power n) - (1 / 2) <= Lucas n by FIB_NUM3:21;
tau_bar to_power n < 1 / 2 by Th8, A1;
then (tau_bar to_power n) + (tau to_power n) < (1 / 2) + (tau 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 7; :: thesis: verum