proposition: Lemma components_subset (G : sgraph) (U C : {set G}) : C \in components U -> C \subset U.
proof: Proof. move => comp_C. case/and3P : (partition_components U) => /eqP <- _ _. apply/subsetP => x. exact: mem_cover. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)