proposition: Lemma Zeck_fib1 n: Zeck (fib n.*2.+1).-1 = rev (mkseq double n).
proof: Proof. rewrite - fib_sum_even_alt2 - Zeckv_rev; apply: (ZeckP (sorted_ggen_sdouble n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)