proposition: Lemma leq_count_subseq P s1 s2 : subseq s1 s2 -> count P s1 <= count P s2.
proof: Proof. by move=> /subseqP[m _ ->]; rewrite leq_count_mask. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)