proposition: Lemma setIPn (T : finType) (A B : {set T}) (x:T) : reflect (x \notin A \/ x \notin B) (x \notin A :&: B).
proof: Proof. rewrite !inE negb_and. exact: orP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries)