proposition: Lemma flatten_imageP (aT : finType) (rT : eqType) (A : aT -> seq rT) (P : {pred aT}) (y : rT) : reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P]).
proof: Proof. by apply: (iffP flatten_mapP) => [][x Px]; exists x; rewrite ?mem_enum in Px *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)