proposition: Lemma big_fset0 (P : pred fset0) (F : @fset0 I -> R) : \big[op/idx]_(i : fset0 | P i) F i = idx.
proof: Proof. by rewrite /index_enum -enumT /= enum_fset0 big_nil. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)