proposition: Lemma component_of_components (G : sgraph) (x : G) : component_of x \in components [set: G].
proof: Proof. by rewrite pblock_mem // (cover_partition (D := setT)). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)