proposition: Lemma Zeckp_fibb n: Zeckp (fib n.*2.+1).-2 = (fib n.*2).-1.
proof: Proof. rewrite -fib_sum_odd_alt - (fib_sum_even_alt2 n) /Zeck_val /Zeck_valp /mkseq. case: n; first by rewrite !big_nil Zeckp_0. move => n; rewrite !map_cons !big_cons !add1n !succnK -/iota. apply: Zeckp_prop1; apply: (mkseq_uniq _ _ double_inj). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)