proposition: Lemma Zeck_valp_cv1 B (t:{set 'I_B.+1}) : Zeck_valp (seto_to_seq t) = Zeck_svalp t.
proof: Proof. exact: Zeck_val_cv0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)