proposition: Lemma treewidth_K_free (G : sgraph) (T : forest) (B : T -> {set G}) m : sdecomp T G B -> width B <= m -> ~ minor G 'K_m.+1.
proof: Proof. move => decT wT M. case: (width_minor decT M) => B' [B1 B2]. suff: m < m by rewrite ltnn. apply: leq_trans wT. apply: leq_trans B2. apply: (Km_width B1). Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)