proposition: Lemma Zeckp_fiba n: Zeckp (fib (n.*2.+1)).-1 = fib n.*2.
proof: Proof. rewrite -fib_sum_odd_alt -fib_sum_even_alt2. 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)