proposition: Lemma eq_fbigl_cond (A B : {fset I}) (P Q : pred I) (F : I -> R) : [fset x in A | P x] =i [fset x in B | Q x] -> \big[op/idx]_(i <- A | P i) F i = \big[op/idx]_(i <- B | Q i) F i.
proof: Proof. by move=> AB; apply: eq_fbig_cond. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)