proposition: Lemma big1_fset (X : {fset I}) (P : pred I) (F : I -> R) : (forall i, i \in X -> P i -> F i = idx) -> \big[op/idx]_(i <- X | P i) F i = idx.
proof: Proof. by move=> Fid; rewrite big_seq_fsetE big1//= => -[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)