proposition: Lemma fib_sum_alt n: Zeck_val (iota 0 n) = (fib (n.+3)).-2.
proof: Proof. rewrite - fib_sum /Zeck_val. have <-:(\sum_(0 <= i0 < n.+2) fib i0) = (\sum_(i0 < n.+2) fib i0). by rewrite big_mkord. rewrite big_nat_recl // add0n big_nat_recl // add1n /= big_mkord. elim: n; first by rewrite big_nil big_ord0. by move => k H; rewrite iota_Sr 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)