proposition: Lemma imsetD (A B : {set aT}) : {in A :|: B &, injective f} -> f @: (B :\: A) = (f @: B) :\: (f @: A).
proof: Proof. move=> injf; apply/setP=> y; rewrite inE. apply/imsetP/andP => [[x] | [yNfA] /imsetP[x xB Hy]]. - rewrite inE => /andP[xNA xB ->{y}]; split; last exact: imset_f. move: xNA; apply contra. by move=> /imsetP[x1 x1A] /injf->; rewrite ?inE ?xB ?x1A ?orbT. - subst y; exists x; rewrite // inE xB andbT. by move: yNfA; apply contra; apply imset_f. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)