proposition: Lemma fsetUDU (T : choiceType) (A B C : {fset T}) : [disjoint A & B] -> (A `|` B) `\` (A `|` C) = B `\` C.
proof: Proof. move => disAC. apply/fsetP => x. rewrite !inE. case Hx : (x \in A) => //=. by rewrite -[x \in B]negbK (fdisjointP disAC) //= andbF. Qed.
imports: mathcomp(all_ssreflect)