proposition: Lemma filter_pred1_uniq s x : uniq s -> x \in s -> filter (pred1 x) s = [:: x].
proof: Proof. move=> uniq_s s_x; rewrite (all_pred1P _ _ (filter_all _ _)). by rewrite size_filter count_uniq_mem ?s_x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)