fact: Definition disconnected (G : sgraph) (S : {set G}) := exists x y : G, [/\ x \in S, y \in S & ~~ connect (restrict S edge_rel) x y].
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)