proposition: Lemma component_can_v : cancel component_v component_v'.
proof: Proof. case => a; rewrite /component_v/component_v'; case: (decC _) => p. - congr inl. exact: val_inj. - exfalso. move: (valP a) => /= X. by rewrite inE X in p. - exfalso. move: (valP a) => /=. by rewrite inE p. - congr inr. exact: val_inj. 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)