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