proposition: Lemma width_link (G : sgraph) (D : T -> {set G}) (A : {set G}) : width (decompL D A) <= maxn (width D) #|A|.
proof: Proof. apply/bigmax_leqP => [] [t|] _ /=; last by rewrite ?leq_maxr. apply: leq_trans (leq_maxl _ _). exact: leq_bigmax. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)