proposition: Lemma setDK (T : finType) (A B : {set T}) : B \subset A -> (A :\: B :|: B) = A.
proof: Proof. by move => subBA; rewrite setDE setUIl (setUidPl subBA) setUC setUCr setIT. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)