proposition: Lemma subset_clns : D1 \subset D2 -> NS[D1] \subset NS[D2].
proof: Proof. move => D1subD2. by rewrite -(setID D2 D1) (setIidPr _) // /closed_neigh_set bigcup_setU subsetUl. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)