proposition: Lemma Zeckv_bound0 n l : path gtn n l -> (Zeck_val (n::l)).+2 <= fib (n.+4).
proof: Proof. elim: l n => [n _ | a l Hrec /= n/andP []]. rewrite Zeckv_cons Zeckv_nil - addnS - addnS (fibSS n.+2) addnC. by rewrite leq_add2r (@fib_monotone 3). rewrite - 3!ltnS => /fib_monotone la /Hrec lb. by rewrite fibSS addnC Zeckv_cons -addnS ltn_add2l (leq_trans lb la). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)