proposition: Lemma flatten_single x l : uniq l -> x \in l -> (forall y, y \in l -> y != x -> f y = [::]) -> flatten (map f l) = f x.
proof: Proof. elim: l => [|a l IH] //= /andP [Hal Hun] Hx Hy. move: Hx. rewrite in_cons => /orP [/eqP|] Hx. suff ->: flatten (map f l) = [::]. by rewrite cats0 Hx. apply/nilP; rewrite /nilp size_flatten sumnE !big_map big_seq big1 //. move=> i Hi; apply/eqP/nilP/Hy. - by rewrite in_cons Hi orbT. - by subst x; apply: contra Hal => /eqP <-. rewrite Hy //=. - apply IH => // y Hyl; apply Hy. by rewrite in_cons Hyl orbT. - by apply mem_head. - by apply: contra Hal => /eqP ->. Qed.
imports: mathcomp(all_ssreflect fingroup perm)