proposition: Lemma filter_uniq s a : uniq s -> uniq (filter a s).
proof: Proof. elim: s => //= x s IHs /andP[s'x]; case: ifP => //= a_x /IHs->. by rewrite mem_filter a_x s'x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)