fact: Definition iso_component : iso (union (induced C) (induced (~: C))) G := Eval hnf in Iso' component_can_v component_can_v' component_can_e component_can_e' component_hom.
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)