proposition: Lemma fib_partial_sum' k n (L := k:: mkseq (fun i => (k.+1+ i.*2)) n) : Zeck_val L = fib (k.+2 + n.*2) /\ sorted gespec (rev L).
proof: Proof. split; last by exact (proj2 (fib_partial_sum k n)). rewrite -(proj1 (fib_partial_sum k.+2 n)). rewrite /Zeck_val /L !big_cons ! big_map //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)