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