proposition: Lemma big_fset (X : finmempred _) (P : pred I) (F : I -> R) : \big[op/idx]_(i <- [fset i in X | P i]) F i = \big[op/idx]_(i <- enum_finmem X | P i) F i.
proof: Proof. by rewrite !eq_big_imfset//= !big_map !big_filter_cond big_andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)