proposition: Lemma setUD (B A C : {set V}) : B \subset A -> C \subset B -> (A :\: B) :|: (B :\: C) = (A :\: C).
proof: Proof. move=> subBA subCB; apply/setP=> x; rewrite !inE. have /implyP := subsetP subBA x; have /implyP := subsetP subCB x. by do !case: (_ \in _). Qed.
imports: HB(structures) mathcomp(all_ssreflect)