proposition: Lemma double_lucas: forall n, 3 <= n -> (lucas n).*2 = fib (n.+3) + fib (n-3).
proof: Proof. case=> [|[|[|n]]] // _; rewrite !subSS subn0. apply/eqP. rewrite -(eqn_add2l (lucas n.+4)) [X in _ == X + _]lucasSS addnC -addnn. rewrite -2![lucas _ + _ + _]addnA eqn_add2l addnC -lucasSS. rewrite !lucas_fib // [_ + (_ + _)]addnC -[fib _ + _ + _]addnA eqn_add2l. by rewrite [_ + (_ + _)]addnC -addnA -fibSS. Qed.
imports: mathcomp(all_ssreflect all_algebra)