proposition: Lemma opns_sub_clns : NS(D1) \subset NS[D1].
proof: Proof. apply/subsetP => u /bigcupP [v vinD1 uinNv]. apply/bigcupP; exists v => //; by rewrite /closed_neigh in_setU uinNv orbT. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)