proposition: Lemma induced_minor : minor G (induced S).
proof: Proof. exact: minor_of_rmap induced_rmapP. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)