proposition: Lemma remove_edges_sub : subgraph (remove_edges E) G.
proof: Proof. exists id, val, xpred0; split=> //; split; first exact: inj_id; exact: val_inj. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)