proposition: Lemma remove_edge_add (G : graph) (e : edge G) : remove_edges [set e] ∔ [source e, elabel e, target e] ≃ G.
proof: Proof. Iso bij_id (bijD1 e) xpred0. constructor => //. - by case => [f b|[|]]. - by case => [f|] /=. Defined.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)