proposition: Lemma double_lucas n: 3 <= n -> (lucas n).*2 = fib (n.+3) + fib (n-3).
proof: Proof. case:n => [|[|[|n]]] // _ ; rewrite !subSS subn0. rewrite fibSS fibSS -addnA addnAC addnA addnn lucas_fib //= doubleD - addnA. by rewrite (addnC (fib n)) (fibSS n.+1) - addnA -fibSS addnn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)