proposition: Lemma leq_uniq_countP x s1 s2 : uniq s1 -> reflect (x \in s1 -> x \in s2) (count_mem x s1 <= count_mem x s2).
proof: Proof. move/count_uniq_mem->; case: (boolP (_ \in _)) => //= _; last by constructor. by rewrite -has_pred1 has_count; apply: (iffP idP) => //; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)