proposition: Lemma big_partition {aT rT : eqType} {R : Type} {idx : R} {op : Monoid.com_law idx} {F : aT -> R} {l : seq aT} {s : seq rT} {f : aT -> rT} : uniq s -> all (fun x=> f x \in s) l -> \big[op/idx]_(i <- l) F i = \big[op/idx]_(y <- s) \big[op/idx]_(i <- l | f i == y) F i.
proof: Proof. move=>us fs. move:(@big_allpairs_dep _ idx op _ _ _ (fun i j=> j) s (fun i=> [seq j <- l | f j == i]) F); congr eq. by apply/perm_big/perm_eq_partition. by apply congr_big=>//y _; rewrite big_filter. Qed.
imports: mathcomp(all_ssreflect ssrnum zmodp order constructive_ereal) preliminaries