fact: Definition igraph (G : graph) (x y : skeleton G) := @point (subgraph_for (@igraph_proof G x y)) (Sub x (intervalL x y)) (Sub y (intervalR x 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)