fact: Definition interval_edges (G : graph) (x y : G) := edge_set (@interval G x y) :\: (edges x x :|: edges y y).
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)