proposition: Lemma fib_partial_sum k n (L := k:: mkseq (fun i => (k.+1+ i.*2)) n) : \sum_(i <- L) (fib i) = fib (k + n.*2) /\ sorted gespec (rev L).
proof: Proof. have A i j: j + (i.+1).*2 = j.+2 + i.*2. by rewrite doubleS - add2n addnA - (addn2 j). rewrite /L big_cons; clear L;split. elim:n k; first by move => k; rewrite /mkseq /= big_nil !addn0. move => n H k; rewrite /mkseq /= iota_S big_cons addn0 addnA. rewrite (addnC (fib k)) -fibSS A - H ! big_map. by congr addn; apply: eq_bigr => i _; rewrite A. rewrite rev_sorted /=. case: n => // n; elim: n k => [k| n H k]; first by rewrite /= addn0 eqxx. move:(H k.+2) => /= /andP [_]. rewrite A !addn0 !eqxx orbT /= (iota_S 1); congr (path _ k.+3). by rewrite - map_comp; apply/eq_in_map => i _; rewrite /= A. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)