proposition: Lemma del_edges_opn A x z : z \in N(del_edges A;x) = (z \in N(G;x)) && ~~ ([set x; z] \subset A).
proof: Proof. by rewrite !inE -in_edges mem_del_edges in_edges. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)