proposition: Lemma setUPn (T : finType) (A B : {set T}) (x:T) : reflect (x \notin A /\ x \notin B) (x \notin A :|: B).
proof: Proof. rewrite !inE negb_or. exact: andP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries)