proposition: Lemma Zeck_val_cv0 B (t:{set 'I_B.+1}) (f:nat->nat): \sum_(i <- (seto_to_seq t)) f i = \sum_(i in t) f i.
proof: Proof. transitivity (\sum_(i <- (enum t)) (f i)). rewrite /seto_to_seq /Zeck_val;elim (enum t); first by rewrite ! big_nil. by move => a l h; rewrite map_cons !big_cons h. by rewrite big_enum. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)