proposition: Lemma component_can_v' : cancel component_v' component_v.
proof: Proof. by move => x; rewrite /component_v/component_v'; case: (decC x). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient bij preliminaries) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(setoid_bigop structures mgraph mgraph2)