proposition: Lemma flatten_mapP (A : S -> seq T) s y : reflect (exists2 x, x \in s & y \in A x) (y \in flatten (map A s)).
proof: Proof. apply: (iffP flattenP) => [[_ /mapP[x sx ->]] | [x sx]] Axy; first by exists x. by exists (A x); rewrite ?map_f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)