proposition: Lemma leq_count_mask T (P : {pred T}) m s : count P (mask m s) <= count P s.
proof: Proof. by elim: s m => [|x s IHs] [|[] m]//=; rewrite ?leq_add2l (leq_trans (IHs _)) ?leq_addl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)