proposition: Lemma Zeckp_fibd n: Zeckp ((fib n.*2).-2) = (fib n.*2.-1).-1.
proof: Proof. case: n => [| [|n]]; rewrite ?Zeckp_0 //. set L := [seq i.*2.+1 | i <- iota 1 n]. rewrite - fib_sum_odd_alt - fib_sum_even_alt /mkseq /=/ Zeck_valp /Zeck_valpp. rewrite! big_cons add0n addnCA add2n !succnK iota_S - map_comp. rewrite (map_comp succn (fun i => i.*2.+1)) -/L big_map big_map. have sa: sorted llen (1 :: L). rewrite - [(1::L) ] / [seq i.*2.+1 | i <- iota 0 n.+1]. by apply:sorted_llen_mkseq => u /=; rewrite doubleS !ltnS. by rewrite (Zeck_split sa) // Zeckp_1 (Zeckp_prop1 (uniq_llen sa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)