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