proposition: Lemma trivIset_components (G : sgraph) (U : {set G}) : trivIset (components U).
proof: Proof. by case/and3P : (partition_components U). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)