proposition: Lemma max_rep_bound a l: spec_sorted (a::l) -> (fib a.+3).-1 <= Zeck_val (a::l) < (fib a.+4).-1.
proof: Proof. move => h. apply /andP; split; last first. by rewrite -ltnS - fib_pos (Zeckv_bound0 (spec_sorted_sorted h)). elim: l a h. move => a; rewrite Zeckv_cons Zeckv_nil spec_sorted_rec /= andbT. by case: a => //; case. move => a l Hrec b. have H:= (fib_pos b). rewrite spec_sorted_rec /= => /andP[ha /Hrec hb]. rewrite Zeckv_cons fibSS H addnS /= leq_add2l (leq_trans _ hb) //. by case /orP: ha => /eqP <-; rewrite ? leqnn // fibSS {2} H addSn leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)