proposition: Theorem excluded_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][]]. exact: TW2_of_K4F. exact: TW2_K4_free. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)