proposition: Lemma partition_components (G : sgraph) (H : {set G}) : partition (components H) H.
proof: Proof. apply: equivalence_partitionP. exact: (@sedge_equiv_in G). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)