proposition: Lemma undup_filter (P : pred B) l : undup (filter P l) = filter P (undup l).
proof: Proof. elim: l => // h t IH /=; case/boolP : (P h) => /= Ph. - case/boolP: (h \in t) => ht. + by rewrite mem_filter Ph ht. + by rewrite mem_filter (negbTE ht) andbF /= Ph IH. - rewrite IH; case: ifPn => //= ?; by rewrite (negbTE Ph). Qed.
imports: mathcomp(all_ssreflect fingroup perm)