proposition: Lemma big_enumP I P : big_enum_spec P (filter P (index_enum I)).
proof: Proof. set e := filter P _; have Ue: uniq e by apply/filter_uniq/index_enum_uniq. have mem_e i: i \in e = P i by rewrite mem_filter mem_index_enum andbT. split=> // [R idx op F | cP]; first by rewrite big_filter. suffices De: perm_eq e (enum cP) by rewrite (perm_size De) cardE. by apply/uniq_perm=> // [|i]; rewrite ?enum_uniq ?mem_enum ?mem_e. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)