proposition: Lemma leq_uniq_count s1 s2 : uniq s1 -> {subset s1 <= s2} -> (forall x, count_mem x s1 <= count_mem x s2).
proof: Proof. by move=> s1_uniq s1_s2 x; apply/leq_uniq_countP/s1_s2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)