proposition: Lemma del_edges_sub A : E(del_edges A) \subset E(G).
proof: Proof. by apply/subsetP => e; rewrite mem_del_edges => /andP[]. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)