proposition: Lemma lucas_square n: (lucas n)^2 = (if (odd n) then subn else addn) (lucas (n.*2)) 2.
proof: Proof. case:n => // n. set b := fib n.+1 ^ 2. rewrite lucas_fib //= lucas_fib // !fib_doubleS - addnA sqrnD. rewrite (addnA b) addnn (addnC b.*2) addnA mul2n. set a := fib n.+2 * fib n; set c := fib n.+2 ^ 2 + fib n ^ 2. move:(fib_sub (leqnSn n)); rewrite mulnn (subSn (leqnn n)) subnn -/b -/a => h. have: (if odd n then a > b else b > a). by case : odd h; rewrite - subn_gt0 => <-. rewrite -[2]/((fib 1).*2) h; case: odd => /= /ltnW/subnK {1} <-. by rewrite - addnA - doubleD [in (_ + _).*2] addnC. by rewrite doubleD addnCA addKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)