proposition: Lemma del_edges_proper e A : e \in E(G) -> e \subset A -> E(del_edges A) \proper E(G).
proof: Proof. move=> edge_e e_sub_A. rewrite properE del_edges_sub /=. by apply/subsetPn; exists e => //; rewrite mem_del_edges edge_e e_sub_A. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)