proposition: Lemma big_msetn n a P F : \big[op/idx]_(i <- msetn n a | P i) F i = if P a then iterop n op (F a) idx else idx.
proof: Proof. by rewrite enum_msetn big_nseq_cond Monoid.iteropE. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap