proposition: Corollary minor_exclusion_2p (G : graph2) : K4_free (sskeleton G) <-> exists (T : forest) (B : T -> {set G}), [/\ sdecomp T (sskeleton G) B & width B <= 3].
proof: Proof. split => [K4F_G|[T [B [B1 B2 B3]]]]. - have [T [B] [B1 B2]] := (graph_of_TW2 (term_of' G)). have I := term_of_iso' K4F_G. symmetry in I. apply sskel_iso2 in I. have [D D1 D2] := decomp_iso B1 I. exists T. exists D. by rewrite D2. - exact: TW2_K4_free B1 B2 B3. 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)