proposition: Lemma mem_del_edges e A : e \in E(del_edges A) = (e \in E(G)) && ~~ (e \subset A).
proof: Proof. apply/edgesP/andP => [[x] [y] [-> /andP[xy xyA]]|[]]; first by rewrite in_edges. by move/edgesP => [x] [y] [-> xy xyNA]; exists x,y; split => //; apply/andP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)