proposition: Lemma filter_undup p s : filter p (undup s) = undup (filter p s).
proof: Proof. elim: s => //= x s IHs; rewrite (fun_if undup) fun_if /= mem_filter /=. by rewrite (fun_if (filter p)) /= IHs; case: ifP => -> //=; apply: if_same. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)