proposition: Lemma imfsetU (aT rT : choiceType) (f : aT -> rT) (A B : {fset aT}) : [fset f x | x in A `|` B] = [fset f x | x in A] `|` [fset f x | x in B].
proof: Proof. apply/fsetP => z. rewrite inE. apply/imfsetP/idP. - case => x0. rewrite !inE. case/orP => H ->; first by rewrite in_imfset. by rewrite [X in _ || X]in_imfset // orbT. - case/orP. all:case/imfsetP => z0 /= H ->; exists z0 => //. all: by rewrite !inE H ?orbT. Qed.
imports: mathcomp(all_ssreflect)