proposition: Lemma in_component_of (G : sgraph) (x : G) : x \in component_of x.
proof: Proof. by rewrite mem_pblock (cover_partition (D := setT)). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)