proposition: Lemma count_mem_uniq s : (forall x, count_mem x s = (x \in s)) -> uniq s.
proof: Proof. move=> count1_s; have Uus := undup_uniq s. suffices: perm_eq s (undup s) by move/perm_uniq->. by apply/allP=> x _; apply/eqP; rewrite (count_uniq_mem x Uus) mem_undup. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)