proposition: Lemma fib_double n: fib ((n.+1).*2) = (fib n.+1) *((fib n).*2 + fib (n.+1)).
proof: Proof. by rewrite fib_double_lucas lucasS addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)