proposition: Lemma Zeckv_bnd l i: i \in l -> i <= Zeck_val l.
proof: Proof. rewrite Zeck_valppE=> /Zeckvp_bnd/leq_trans -> //; exact: leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)