proposition: Lemma mem_clns u v : u \in D1 -> u -- v -> v \in NS[D1].
proof: Proof. move=> uinD1 adjuv; apply: (subsetP opns_sub_clns). exact: mem_opns adjuv. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)