proposition: Lemma del_edges1 e : e \in E(G) -> E(G) = e |: E(del_edges e).
proof: Proof. move => edge_e; apply/setP => e'; rewrite in_setU mem_del_edges in_set1. case: (eqVneq e e') => [<-//|eDe'/=]. case: (boolP (e' \in E(G))) => //= edge_e'; symmetry. rewrite eq_sym in eDe'; exact: edges_eqn_sub eDe'. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)