fact: Definition components (G : sgraph) (H : {set G}) : {set {set G}} := equivalence_partition (connect (restrict H (--))) H.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)