proposition: Lemma opn_edges (u : G) : N(u) = [set v | [set u; v] \in E(G)].
proof: Proof. apply/eqP ; rewrite eqEsubset ; apply/andP ; split. - by apply/subsetP=> w ; rewrite in_opn in_set in_edges. - by apply/subsetP=> w ; rewrite in_opn in_set in_edges. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)