proposition: Lemma filter_flatten ss (P : pred T) : filter P (flatten ss) = flatten [seq filter P i | i <- ss].
proof: Proof. by elim: ss => // s ss /= <-; apply: filter_cat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)