proposition: Lemma small_K_free m (G : sgraph): #|G| <= m -> ~ minor G 'K_m.+1.
proof: Proof. move => H. case: (decomp_small H) => T [D] [decD wD]. exact: treewidth_K_free decD wD. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)