proposition: Lemma partition_big_imfset (h : I -> J) (A : {fset I}) (F : I -> R) : \big[op/idx]_(i <- A) F i = \big[op/idx]_(j <- [fset h x | x in A]) \big[op/idx]_(i <- A | h i == j) F i.
proof: Proof. transitivity (\big[op/idx]_(i <- [fset (h i, i) | i in A]) F i.2). by rewrite eq_big_imfset ?big_map// => i j ? ? []. transitivity (\big[op/idx]_(i <- [fset ij | ij in [seq (i1, i2) | i1 <- [fset h x | x in A], i2 <- A]]) if h i.2 == i.1 then F i.2 else idx). rewrite -big_mkcond; apply: eq_fbigl_cond; move=> x; rewrite !inE/= andbT. apply/imfsetP/idP => [[i /= iA -> /=]|]. rewrite eqxx andbT; apply/allpairsP; exists (h i, i) => /=. by rewrite in_imfset. by move=> /andP[/allpairsP[[/= j i] [/imfsetP[/=a aA ->] iA ->/= /eqP<-]]]; exists i. rewrite eq_big_imfset //= big_map undup_id. by rewrite big_allpairs; apply: eq_bigr => i /= _; rewrite -big_mkcond. by rewrite allpairs_uniq => //= -[j0 i0] [j1 i1] /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)