proposition: Lemma fib_double_lucas n: fib (n.*2) = fib n * lucas n.
proof: Proof. case:n=> [|n]; rewrite // -addnn fib_add // lucas_fib // mulnDr addnC /=. by rewrite (mulnC (fib n)(fib n.+1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)