proposition: Lemma count_flatten ss P : count P (flatten ss) = sumn [seq count P x | x <- ss].
proof: Proof. by elim: ss => //= s ss IHss; rewrite count_cat IHss. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)