proposition: Lemma undup_perm (f : A -> B) p h t : undup (map f p) = h :: t -> exists p1 : seq A, exists p2 : seq A, perm_eq p (p1 ++ p2) /\ undup (map f p1) = [:: h] /\ undup (map f p2) = t.
proof: Proof. move=> p_t; exists (filter (preim f (pred1 h)) p), (filter (preim f (mem t)) p). split. - apply/permPl => x; rewrite -(perm_filterC (preim f (pred1 h)) p). apply/permPl : x. rewrite perm_cat2l (@eq_in_filter _ _ [pred x | f x \in t]) //= => x X. case/boolP: (f x == h) => [/eqP ->|/negbTE fxh] /=; apply/esym. + by have /andP[/negbTE] : uniq (h :: t) by rewrite -p_t; apply undup_uniq. + have : f x \in h :: t by rewrite -p_t mem_undup; apply/mapP; exists x. rewrite in_cons => /orP[|->//]; by rewrite fxh. - split. + rewrite -filter_map undup_filter p_t /= eqxx; congr cons. rewrite -(filter_pred0 t); apply eq_in_filter => i it /=. apply/negP => /eqP X; subst h. have : uniq (i :: t) by rewrite -p_t; exact: undup_uniq. rewrite /= => /andP[]; by rewrite it. + rewrite -filter_map undup_filter p_t /= ifF; last first. apply/negP => X. have : uniq (h :: t) by rewrite -p_t undup_uniq. by rewrite /= X. rewrite -[RHS](filter_predT t); exact: eq_in_filter. Qed.
imports: mathcomp(all_ssreflect fingroup perm)