proposition: Lemma Km_width m (T : forest) (D : T -> {set 'K_m.+1}) : sdecomp T 'K_m.+1 D -> m.+1 <= width D.
proof: Proof. case/Km_bag => t Ht. apply: leq_trans Ht _. exact: leq_bigmax. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)