proposition: Lemma del_edgesN e : e \notin E(del_edges e).
proof: Proof. by rewrite mem_del_edges subxx andbF. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)