proposition: Lemma imsetU (A B : {set aT}) : f @: (A :|: B) = (f @: A) :|: (f @: B).
proof: Proof. apply/eqP; rewrite eqEsubset subUset. rewrite 2?imsetS (andbT, subsetUl, subsetUr) // andbT. apply/subsetP=> _ /imsetP[x ABx ->]; apply/setUP. by case/setUP: ABx => [Ax | Bx]; [left | right]; apply/imsetP; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)