proposition: Lemma Zeck_val_cv2 l B (n := Zeck_val l): uniq l -> n <= B -> n = Zeck_sval (seq_to_seto B l).
proof: Proof. move => sa sb. symmetry;rewrite - Zeck_val_cv1; apply: perm_big; apply:(seq_to_setoK sa). apply /allP => i /Zeckv_bnd lin; rewrite ltnS; apply: (leq_trans lin sb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)