proposition: Lemma opn_cln u : N(u) = N[u] :\ u.
proof: Proof. by apply/setP => v; rewrite !inE; case: (eqVneq u v ) => //= ->; rewrite sgP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)