proposition: Lemma Zeck_fib3 k: Zeck (fib (k.+2).*2).-2 = rev(0 :: mkseq (fun i=> i.*2.+3) k).
proof: Proof. set s := [seq i.*2.+3 | i <- iota 0 k]. rewrite - (fib_sum_odd_alt) /Zeck_valp /mkseq /= !big_cons /=. transitivity (Zeck (Zeck_val(0:: s))). by rewrite /s /Zeck_val iota_S iota_S !big_map // big_cons big_map. rewrite - Zeckv_rev; apply: ZeckP; rewrite rev_sorted /s/=; case k => // m. have //:(sorted llen [seq i.*2.+3 | i <- iota 0 m.+1]). by apply:sorted_llen_mkseq => u /=; rewrite doubleS !ltnS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)