proposition: Lemma count_subseqP s1 s2 : (forall x, count_mem x s1 <= count_mem x s2) <-> exists2 s, subseq s s2 & perm_eq s1 s.
proof: Proof. rewrite count_maskP; split=> [[m _]|[_/subseqP[m sm ->]]]; last by exists m. by exists (mask m s2); rewrite ?mask_subseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)