proposition: Lemma mem_component (G : sgraph) (C : {set G}) x : C \in components [set: G] -> x \in C -> C = component_of x.
proof: Proof. move => comp_C inC. symmetry. exact: def_pblock. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)