proposition: Lemma eq_fbig_cond (A B : {fset I}) (P Q : pred I) (F G : I -> R) : [fset x in A | P x] =i [fset x in B | Q x] -> (forall x, x \in A -> P x -> F x = G x) -> \big[op/idx]_(i <- A | P i) F i = \big[op/idx]_(i <- B | Q i) G i.
proof: Proof. move=> /fsetP eqABPQ FG; rewrite big_fset_condE [in RHS]big_fset_condE -eqABPQ. rewrite big_seq_cond [in RHS]big_seq_cond; apply: eq_bigr => i. by rewrite in_fset !inE => /andP[/andP[??] _]; apply: FG. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)