proposition: Lemma Zeckv_bnd0 l i: i \in l -> fib (i.+2) <= Zeck_val l.
proof: Proof. elim: l i => // [a l Hrec i /=]; rewrite in_cons Zeckv_cons; case/orP. move /eqP => ->; case: a => // a; apply: leq_addr. move/Hrec/leq_trans => -> //; exact:leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)