fact: Definition istart (G : sgraph) (x y : G) : igraph x y := Sub x (intervalL x y).
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph minor) GraphTheory(checkpoint connectivity excluded set_tac)