proposition: Lemma opn_proper_cln v : N(v) \proper N[v].
proof: Proof. apply/properP; rewrite subsetUr; split => //. by exists v; rewrite !inE ?eqxx sgP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)