proposition: Lemma in_cln u v : u \in N[v] = (v -*- u).
proof: Proof. by rewrite /closed_neigh in_setU1 eq_sym in_opn. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)