proposition: Lemma minor_trans : Transitive minor.
proof: Proof. move => G H I /minorRE [f mm_f] /minorRE [g mm_g]. apply: minor_of_rmap. exact: minor_rmap_comp mm_f mm_g. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)