proposition: Lemma add_edge_separation_minor M : minor (@induced G' V1) M -> minor G M.
proof: Proof. move=> minorM. suff [phi]: exists2 phi : M -> {set G'}, minor_rmap phi & forall u, phi u \subset V1. exact: add_edge_rmap_separation_minor. case/minorRE : minorM => phi rmap_phi. pose phi' (u : M) := \bigcup_(v in phi u) induced_rmap v : {set G'}. exists phi'; first by apply: minor_rmap_comp => //; apply: induced_rmapP. move=> u. apply/bigcupsP=> v ?. exact: induced_rmap_sub. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)