proposition: Lemma perm_eq_partition {aT rT : eqType} (l : seq aT) (s : seq rT) (f : aT -> rT) : uniq s -> all (fun x=> f x \in s) l -> perm_eq [seq x | y <- s, x <- [seq x <- l | f x == y]] l.
proof: Proof. elim: s l; first by case. move=>y s IHs l yus /allP fl /=. move: (perm_filterC (fun x=> f x == y) l)=>/(_ l); rewrite perm_refl; apply perm_trans. rewrite map_id; apply perm_cat=>//. have->: [seq x | y0 <- s, x <- [seq x <- l | f x == y0]] = [seq x | y0 <- s, x <- [seq x <- [seq x <- l | predC (fun x : aT => f x == y) x] | f x == y0]]. clear IHs fl. elim: s y yus=>// y' s IHl y /andP[]; rewrite in_cons negb_or=> /andP [yy' ys] /andP[_ us] /=; congr cat; last by apply/IHl/andP; split. rewrite 2!map_id -filter_predI; apply eq_filter=>x. apply/idP/idP. by move=>/=/eqP->; rewrite eq_refl eq_sym. by move=>/andP[]. apply IHs; first by move:yus=>/andP[]. by apply/allP=>x; rewrite mem_filter=>/andP [/= /negPf fxy /fl]; rewrite in_cons=>/orP; case=>//; rewrite fxy. Qed.
imports: mathcomp(all_ssreflect ssrnum zmodp order constructive_ereal) preliminaries