proposition: Lemma Km_bag m (T : forest) (D : T -> {set 'K_m.+1}) : sdecomp T 'K_m.+1 D -> exists t, m.+1 <= #|D t|.
proof: Proof. move => decD. case: (@decomp_clique _ _ _ decD setT _ _) => //. - by rewrite cardsT card_ord. - move => t A. exists t. rewrite -{1}[m](card_ord m) -cardsT. apply: leq_trans (subset_leq_card A). by rewrite !cardsT !card_ord. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)