proposition: Lemma fib_sum_even_alt n: Zeck_valpp (mkseq double n) = (fib (n.*2.-1)).-1.
proof: Proof. rewrite -fib_sum_even /Zeck_valpp; elim: n; first by rewrite big_nil big_ord0. by move => n H; rewrite /= mkseq_succ sum_rcons addnC H big_ord_recr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)