proposition: Lemma component_can_e : cancel component_e component_e'.
proof: Proof. case => e; rewrite /component_e/component_e'; case: (decE _) => p. - congr inl. exact: val_inj. - exfalso. move: (valP e) => /= /edge_setN X. by contrab. - exfalso. move: (valP e) => /= X. move/edge_setN in p. by rewrite X in 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)