proposition: Corollary graph_minor_TW2 (G : sgraph) : K4_free G <-> exists (T : forest) (B : T -> {set G}), sdecomp T G B /\ width B <= 3.
proof: Proof. split=> [| [T][B][]]; last exact: TW2_K4_free. case: (posnP #|G|) =>[G_empty | /card_gt0P[x _]]. { exists tunit; exists (fun _ => [set: G]). split; first exact: triv_sdecomp. apply: leq_trans (width_bound _) _. by rewrite G_empty. } move=>HG. have [G' [iso_G _]] := flesh_out (0 : flat nat) tt x. apply (iso_K4_free iso_G) in HG. apply minor_exclusion_2p in HG as (T&B&D&W). case: (decomp_iso D iso_G) => B' D' W'. exists T. exists B'. by rewrite W'. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)