proposition: Lemma big_enum_in_nocond : \big[op/idx]_(i <- enum A) F i = \big[op/idx]_(i in A) F i.
proof: Proof. by rewrite big_filter. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist