proposition: Lemma decomp_small (G : sgraph) k : #|G| <= k -> exists T D, [/\ sdecomp T G D & width D <= k].
proof: Proof. exists tunit; exists (fun => setT). split. - exact: triv_decomp. - by rewrite /width (big_pred1 tt _) // cardsT. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)