proposition: Lemma components_nonempty (G : sgraph) (U C : {set G}) : C \in components U -> exists x, x \in C.
proof: Proof. case: (set_0Vmem C) => [->|[x inC] _]; by [rewrite (partition0 U)| exists x]. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)