proposition: Lemma fib_sum_odd_alt n: Zeck_valp (mkseq double n) = fib (n.*2).
proof: Proof. rewrite -fib_sum_odd /Zeck_valp; 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)