proposition: Lemma Zeckp_fibc n: Zeckp (fib n.*2).-1 = (fib n.*2.-1).-1.
proof: Proof. case: n => [| n]; rewrite ? Zeckp_0 // -fib_sum_odd_alt -fib_sum_even_alt2. set L := [seq z.*2.+1 | z <- iota 0 n]. rewrite /Zeck_valp/mkseq map_cons -/iota iota_S big_cons add1n succnK !big_map. transitivity (Zeckp (Zeck_val L)); first by rewrite /L /Zeck_val big_map. transitivity (Zeck_valp L); last by rewrite /Zeck_val /Zeck_valp !big_map. apply:Zeckp_prop1; apply: (mkseq_uniq _ _ doubleS_inj). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)