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