proposition: Lemma fib_sum_even n: \sum_(i < n) fib i.*2 = (fib n.*2.-1).-1.
proof: Proof. elim:n => [|n IH]; first by rewrite big_ord0. rewrite big_ord_recr IH; case: (n)=> [|n1] //. rewrite (fibSS (n1.*2.+1)) addnC -[(n1.+1).*2.-1]/n1.*2.+1. by case: fib (fib_gt0 (ltn0Sn ((n1.*2)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)