proposition: Lemma count_maskP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) <-> exists2 m : bitseq, size m = size s2 & perm_eq s1 (mask m s2).
proof: Proof. split=> [s1_le|[m _ /permP s1ms2 x]]; last by rewrite s1ms2 leq_count_mask. suff [m mP]: exists m, perm_eq s1 (mask m s2). by have [m' sm' eqm] := resize_mask m s2; exists m'; rewrite -?eqm. elim: s2 => [|x s2 IHs]//= in s1 s1_le *. by exists [::]; apply/allP => x _/=; rewrite eqn_leq s1_le. have [y|m s1s2] := IHs (rem x s1); first by rewrite count_mem_rem leq_subLR. exists ((x \in s1) :: m); have [|/rem_id<-//] := boolP (x \in s1). by move/perm_to_rem/permPl->; rewrite perm_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)