fact: Definition connected (G : sgraph) (S : {set G}) := {in S & S, forall x y : G, connect (restrict S edge_rel) x y}.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)