proposition: Lemma Zeck_fib2 n: Zeck (fib n.*2.+2).-1 = rev (succ_seq (mkseq double n)).
proof: Proof. rewrite - doubleS -fib_sum_odd_alt /Zeck_valp /mkseq /= big_cons add1n succnK. transitivity (Zeck (Zeck_val(rev (succ_seq [seq i.*2 | i <- iota 0 n])))). by rewrite iota_S /Zeck_val /succ_seq sum_rev !big_map. by apply:ZeckP; rewrite rev_sorted sorted_llen_succ sorted_llen_mkseq_e. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)