proposition: Lemma imset_cover (T' : finType) P (f : T -> T') : [set f x | x in cover P] = \bigcup_(i in P) [set f x | x in i].
proof: Proof. apply/setP=> y; apply/imsetP/bigcupP => [|[A AP /imsetP[x xA ->]]]. by move=> [x /bigcupP[A AP xA] ->]; exists A => //; rewrite imset_f. by exists x => //; apply/bigcupP; exists A. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)