proposition: Lemma add_edge_separation_excluded M : ~ minor G M -> ~ minor (@induced G' V1) M.
proof: Proof. exact/contra_not/add_edge_separation_minor. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)