# Library GraphTheory.minor

Require Import RelationClasses.

From mathcomp Require Import all_ssreflect.
Require Import edone preliminaries digraph sgraph treewidth.
Require Import set_tac.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope quotient_scope.
Set Bullet Behavior "Strict Subproofs".

# Minors

H is a minor of G -- The order allows us to write minor G for the collection of Gs minors

Definition minor_map (G H : sgraph) (phi : G option H) :=
[/\ ( y : H, x : G, phi x = Some y),
( y : H, connected (phi @^-1 Some y)) &
( x y : H, x -- y x0 y0 : G,
[/\ x0 \in phi @^-1 Some x, y0 \in phi @^-1 Some y & x0 -- y0])].

Definition minor_rmap (G H : sgraph) (phi : H {set G}) :=
[/\ ( x : H, phi x != set0),
( x : H, connected (phi x)),
( x y : H, x != y [disjoint phi x & phi y]) &
( x y : H, x -- y neighbor (phi x) (phi y))].

Lemma minor_map_rmap (G H : sgraph) (phi : H {set G}) :
minor_rmap phi minor_map (fun x : G[pick x0 : H | x \in phi x0]).
Proof.
set phi' := (fun x_).
caseP1 P2 P3 P4.
have phiP x x0 : x0 \in phi x = (phi' x0 == Some x).
{ rewrite /phi'. case: pickP ⇒ [x' Hx'|]; last by move→.
rewrite Some_eqE. apply/idP/eqP ⇒ [|<-//].
apply: contraTeq ⇒ /P3 D. by rewrite (disjointFr D Hx'). }
split.
- movey. case/set0Pn : (P1 y) ⇒ y0. rewrite phiP ⇒ /eqP <-. by y0.
- movey x0 y0. rewrite !inE -!phiPH1 H2. move: (P2 y _ _ H1 H2).
apply: connect_monou v. by rewrite /= -!mem_preim !phiP.
- movex y /P4/neighborP [x0] [y0] [*]. x0; y0. by rewrite -!mem_preim -!phiP.
Qed.

Lemma minor_rmap_map (G H : sgraph) (phi : G option H) :
minor_map phi minor_rmap (fun x[set y | phi y == Some x]).
Proof.
set phi' := fun __.
caseP1 P2 P3.
split.
- movex. apply/set0Pn. case: (P1 x) ⇒ x0 H0. x0. by rewrite !inE H0.
- movex u v Hu Hv. move: (P2 x _ _ Hu Hv).
apply: connect_monoa b. by rewrite /= !inE.
- movex y. apply: contraNT ⇒ /pred0Pn [x0 /= /andP[]].
by rewrite -Some_eqE !inE ⇒ /eqP<-/eqP<-.
- movex y /P3 [x0] [y0] [*]. apply/neighborP. x0; y0. by rewrite !inE !mem_preim.
Qed.

Lemma rmap_add_edge_sym (G H : sgraph) (s1 s2 : G) (phi : H {set G}) :
@minor_rmap (add_edge s1 s2) H phi @minor_rmap (add_edge s2 s1) H phi.
Proof.
case ⇒ [P1 P2 P3 P4]; split ⇒ //.
- movex y /P4/neighborP ⇒ [[x'] [y'] [A B C]].
apply/neighborP; x'; y'. by rewrite add_edgeC.
Qed.

Lemma rmap_disjE (G H : sgraph) (phi : H {set G}) x i j :
minor_rmap phi x \in phi i x \in phi j i=j.
Proof.
move ⇒ [_ _ map _] xi. apply contraTeqiNj.
by erewrite (disjointFr (map _ _ iNj)).
Qed.

Definition minor (G H : sgraph) : Prop := phi : G option H, minor_map phi.

Fact minor_of_map (G H : sgraph) (phi : G option H):
minor_map phi minor G H.
Proof. case ⇒ ×. by phi. Qed.

Fact minor_of_rmap (G H : sgraph) (phi : H {set G}):
minor_rmap phi minor G H.
Proof. move/minor_map_rmap. exact: minor_of_map. Qed.

Lemma minorRE G H : minor G H phi : H {set G}, minor_rmap phi.
Proof. casephi /minor_rmap_map D. eexists. exact: D. Qed.

Lemma mem_bigcup (T1 T2 : finType) (F : T1 {set T2}) (P : pred T1) z y :
P y z \in F y z \in \bigcup_(x | P x) F x.
Proof. movePy zF. by apply/bigcupP; y; rewrite ?yA. Qed.
Arguments mem_bigcup [T1 T2 F P z] y _ _.

Lemma minor_rmap_comp (G H K : sgraph) (f : H {set G}) (g : K {set H}) :
minor_rmap f minor_rmap g minor_rmap (fun x\bigcup_(y in g x) f y).
Proof.
move ⇒ [f1 f2 f3 f4] [g1 g2 g3 g4]. split ⇒ [x|x|x1 x2|x1 x2].
- case/set0Pn: (g1 x) ⇒ y Gy; case/set0Pn: (f1 y) ⇒ z Fz.
by apply/set0Pn; z; apply/bigcupP; y.
- movez1 z2 /bigcupP [y1 y1_g z1_f] /bigcupP [y2 y2_g z2_f].
have/connectP [p] := (g2 _ _ _ y1_g y2_g).
elim: p z1 y1 y1_g z1_f ⇒ /= [|y1' p IHp] z1 y1 y1_g z1_f.
+ move_ ?; subst.
apply: connect_restrict_mono; [exact: bigcup_sup y1_g|exact: f2].
+ rewrite -andbA ⇒ /and3P [/andP [H1 H2] H3 H4 H5].
case/neighborP: (f4 _ _ H3) ⇒ a [b] [a_fy1 b_fy1' ab].
apply: connect_trans (IHp _ _ H2 b_fy1' H4 H5).
apply: (@connect_trans _ _ a).
× apply: connect_restrict_mono. apply: bigcup_sup y1_g. exact: f2.
× apply: connect1 ⇒ /=.
by rewrite ab andbT (mem_bigcup y1) ?(mem_bigcup y1').
- move/g3Dx. apply/disjointPz.
case/bigcupPy1 y1_g z_fy1; case/bigcupPy2 y2_g z_fy2.
suff: y1 != y2 by move/f3/disjointP/(_ z); apply.
apply: contraTneq y2_g ⇒ <-. by rewrite (disjointFr Dx).
- move/g4/neighborP ⇒ [y1] [y2] [Y1 Y2 /f4 /neighborP [z1] [z2] [? ? e]].
by apply/neighborP; z1; z2; rewrite (mem_bigcup y1) ?(mem_bigcup y2).
Qed.

Lemma minor_map_comp (G H K : sgraph) (f : G option H) (g : H option K) :
minor_map f minor_map g minor_map (obind g \o f).
Proof.
move⇒ [f1 f2 f3] [g1 g2 g3]. rewrite /comp; split.
- movey. case: (g1 y) ⇒ y'. case: (f1 y') ⇒ x E1 ?.
x. by rewrite E1.
- movez x y. rewrite !inE.
case Ef : (f x) ⇒ [fx|] //= gfx. case Eg : (f y) ⇒ [fy|] //= gfy.
move: (g2 z fx fy). rewrite !inE. case/(_ _ _)/Wrap ⇒ // /connectP ⇒ [[p]].
elim: p x fx Ef gfx ⇒ /= [|a p IH] x fx Ef gfx.
+ move_ ?. subst fy.
move: (f2 fx x y). rewrite !inE Ef Eg. case/(_ _ _)/Wrap ⇒ //.
apply: connect_monoa b /=. rewrite !inE -andbA.
case/and3P ⇒ /eqP→ /eqP→ → /=. by rewrite (eqP gfx) !eqxx.
+ rewrite !inE -!andbA ⇒ /and4P [H1 H2 H3 H4] H5.
case: (f1 a) ⇒ x' Hx'. apply: (connect_trans (y := x')); last exact: IH H5.
move/f3 : (H3) ⇒ [x0] [y0] [X1 X2 X3].
apply: (connect_trans (y := x0)); last apply: (connect_trans (y := y0)).
× move: (f2 fx x x0). rewrite !inE ?Ef ?eqxx in X1 ×. case/(_ _ _)/Wrap ⇒ //.
apply: connect_monou v /=. rewrite !inE -andbA.
case/and3P ⇒ /eqP→ /eqP→ → /=. by rewrite H1.
× apply: connect1. rewrite /= !inE ?X3 ?andbT in X1 X2 ×.
by rewrite (eqP X1) (eqP X2) /= (eqP gfx) eqxx.
× move: (f2 a y0 x' X2). case/(_ _)/Wrap. by rewrite !inE Hx'.
apply: connect_monou v /=. rewrite !inE -andbA.
case/and3P ⇒ /eqP→ /eqP→ → /=. by rewrite H2.
- movex y /g3 [x'] [y'] [Hx' Hy'] /f3 [x0] [y0] [Hx0 Hy0 ?].
x0. y0. rewrite !inE in Hx' Hy' Hx0 Hy0 ×.
split ⇒ //; reflect_eq; by rewrite (Hx0,Hy0) /= (Hx',Hy').
Qed.

Lemma minor_trans : Transitive minor.
Proof.
moveG H I /minorRE [f mm_f] /minorRE [g mm_g].
apply: minor_of_rmap. exact: minor_rmap_comp mm_f mm_g.
Qed.

Definition total_minor_map (G H : sgraph) (phi : G H) :=
[/\ ( y : H, x, phi x = y),
( y : H, connected (phi @^-1 y)) &
( x y : H, x -- y
x0 y0, [/\ x0 \in phi @^-1 x, y0 \in phi @^-1 y & x0 -- y0])].

Definition strict_minor (G H : sgraph) : Prop :=
phi : G H, total_minor_map phi.

Lemma map_of_total (G H : sgraph) (phi : G H) :
total_minor_map phi minor_map (Some \o phi).
Proof. caseA B C. split ⇒ // y. case: (A y) ⇒ x <-. by x. Qed.

Lemma strict_is_minor (G H : sgraph) : strict_minor G H minor G H.
Proof. move ⇒ [phi A]. (Some \o phi). exact: map_of_total. Qed.

Lemma sub_minor (S G : sgraph) : subgraph S G minor G S.
Proof.
move ⇒ [h inj_h hom_h].
pose phi x := if @idP (x \in codom h) is ReflectT p then Some (iinv p) else None.
phi; split.
- movey. (h y). rewrite /phi.
case: {-}_ / idP ⇒ [p|]; by rewrite ?iinv_f ?codom_f.
- movey x0 y0. rewrite !inE {1 2}/phi.
case: {-}_ / idP ⇒ // p /eqP[E1].
case: {-}_ / idP ⇒ // q /eqP[E2].
suff → : (x0 = y0) by exact: connect0.
by rewrite -(f_iinv p) -(f_iinv q) E1 E2.
- movex y A. move/hom_h : (A) ⇒ B.
(h x). (h y). rewrite !inE /phi B.
+ by do 2 case: {-}_ / idP ⇒ [?|]; rewrite ?codom_f ?iinv_f ?eqxx //.
+ apply: contraTneq A ⇒ /inj_h →. by rewrite sgP.
Qed.

Lemma iso_strict_minor (G H : sgraph) : diso G H strict_minor H G.
Proof.
move⇒ [[h g hgK ghK] /= hH gH].
have in_preim_g x y : (y \in g @^-1 x) = (y == h x).
rewrite -mem_preim; exact: can2_eq.
g; split.
+ by movey; (h y); rewrite hgK.
+ movey x1 x2. rewrite !in_preim_g ⇒ /eqP→ /eqP→. exact: connect0.
+ movex y xy. (h x); (h y). rewrite !in_preim_g.
split⇒ //. exact: hH.
Qed.

Induced subgraphs are trivially minors
Section induced_rmap.
Variables (G : sgraph) (S : {set G}).

Definition induced_rmap := (fun x : induced S[set val x]).

Lemma induced_rmapP : minor_rmap induced_rmap.
Proof.
split.
- move⇒ ?; exact: set10.
- move⇒ ?; exact: connected1.
- by move⇒ ? ?; rewrite disjoints1 inE val_eqE.
- by move⇒ ? ?; rewrite neighbor11.
Qed.

Lemma induced_rmap_sub u : induced_rmap u \subset S.
Proof. by rewrite /induced_rmap sub1set; apply: (valP u). Qed.

Lemma induced_minor : minor G (induced S).
Proof. exact: minor_of_rmap induced_rmapP. Qed.

End induced_rmap.

Definition edge_surjective (G1 G2 : sgraph) (h : G1 G2) :=
x y : G2 , x -- y x0 y0, [/\ h x0 = x, h y0 = y & x0 -- y0].

Lemma rename_sdecomp (T : forest) (G H : sgraph) D (dec_D : sdecomp T G D) (h :G H) :
hom_s h surjective h edge_surjective h
( x y, h x = h y t, (x \in D t) && (y \in D t))
@sdecomp T _ (rename D h).
Abort.

Lemma width_minor (G H : sgraph) (T : forest) (B : T {set G}) :
sdecomp T G B minor G H B', @sdecomp T H B' width B' width B.
Proof.
movedecT [phi [p1 p2 p3]].
pose B' t := [set x : H | [ (x0 | x0 \in B t), phi x0 == Some x]].
B'. split.
- split.
+ movey. case: (p1 y) ⇒ x /eqP Hx.
case: (sbag_cover decT x) ⇒ t Ht.
t. apply/pimsetP. by x.
+ movex y xy. move/p3: xy ⇒ [x0] [y0]. rewrite !inE ⇒ [[H1 H2 H3]].
case: (sbag_edge decT H3) ⇒ t /andP [T1 T2]. t.
apply/andP; split; apply/pimsetP; by [ x0| y0].
+ have conn_pre1 t1 t2 x x0 :
phi x0 == Some x x0 \in B t1 x0 \in B t2
connect (restrict [pred t | x \in B' t] sedge) t1 t2.
{ moveH1 H2 H3. move: (sbag_conn decT H2 H3).
apply: connect_monou v /=. rewrite !in_simpl -!andbA ⇒ /and3P [? ? ?].
apply/and3P; split ⇒ //; apply/pimsetP; eexists; eauto. }
movex t1 t2 /pimsetP [x0 X1 X2] /pimsetP [y0 Y1 Y2].
move: (p2 x x0 y0). rewrite !inE. case/(_ _ _)/Wrap ⇒ // /connectP [p].
elim: p t1 x0 X1 X2 ⇒ /= [|z0 p IH] t1 x0 X1 X2.
× move_ E. subst x0. exact: conn_pre1 X1 Y1.
× rewrite -!andbA ⇒ /and3P [H1 H2 /andP [H3 H4] H5].
case: (sbag_edge decT H3) ⇒ t /andP [T1 T2].
apply: (connect_trans (y := t)).
-- move ⇒ {p IH H4 H5 y0 Y1 Y2 X2}. rewrite !inE in H1 H2.
exact: conn_pre1 X1 T1.
-- apply: IH H4 H5 ⇒ //. by rewrite inE in H2.
- apply: bigmax_leq_pointwiset _. exact: pimset_card.
Qed.

Lemma minor_of_clique (G : sgraph) (S : {set G}) n :
n #|S| clique S minor G 'K_n.
Proof.
case/card_geqPs [uniq_s /eqP size_s sub_s clique_S].
pose t := Tuple size_s.
pose phi (i : 'K_n) := [set tnth t i].
suff H: minor_rmap phi by apply (minor_of_map (minor_map_rmap H)).
split.
- movei. apply/set0Pn; (tnth t i). by rewrite !inE.
- movei. exact: connected1.
- movei j iNj. rewrite disjoints1. apply: contraNN iNj.
by rewrite inE tnth_uniq.
- movei j /= ?. apply/neighborP. (tnth t i); (tnth t j).
rewrite !inE !tnth_uniq ?eqxx //.
rewrite clique_S // ?tnth_uniq // ?sub_s //; exact: mem_tnth.
Qed.

Lemma Kn_clique n : clique [set: 'K_n].
Proof. by []. Qed.

Definition K4_free (G : sgraph) := ¬ minor G K4.

Lemma minor_K4_free (G H : sgraph) :
minor G H K4_free G K4_free H.
Proof. moveM F C. apply: F. exact: minor_trans C. Qed.

Lemma subgraph_K4_free (G H : sgraph) :
subgraph H G K4_free G K4_free H.
Proof. move/sub_minor. exact: minor_K4_free. Qed.

Lemma iso_K4_free (G H : sgraph) :
diso G H K4_free H K4_free G.
Proof. moveiso_GH. apply: subgraph_K4_free. exact: iso_subgraph. Qed.

Lemma treewidth_K_free (G : sgraph) (T : forest) (B : T {set G}) m :
sdecomp T G B width B m ¬ minor G 'K_m.+1.
Proof.
movedecT wT M. case: (width_minor decT M) ⇒ B' [B1 B2].
suff: m < m by rewrite ltnn.
apply: leq_trans wT. apply: leq_trans B2. apply: (Km_width B1).
Qed.

Lemma TW2_K4_free (G : sgraph) (T : forest) (B : T {set G}) :
sdecomp T G B width B 3 K4_free G.
Proof. exact: treewidth_K_free. Qed.

Lemma small_K_free m (G : sgraph): #|G| m ¬ minor G 'K_m.+1.
Proof.
moveH. case: (decomp_small H) ⇒ T [D] [decD wD].
exact: treewidth_K_free decD wD.
Qed.

Lemma minor_induced_add_node (G : sgraph) (N : {set G}) : @minor_map (induced [set¬ None : add_node G N]) G val.
Proof.
have inNoneD (a : G) : Some a \in [set¬ None] by rewrite !inE. split.
+ movey. by (Sub (Some y) (inNoneD y)).
+ movey x1 x2. rewrite -!mem_preim =>/eqP<- /eqP/val_inj→. exact: connect0.
+ movex y xy. (Sub (Some x) (inNoneD x)).
(Sub (Some y) (inNoneD y)). by split; rewrite -?mem_preim.
Qed.

Lemma add_node_minor (G G' : sgraph) (U : {set G}) (U' : {set G'}) (phi : G G') :
( y, y \in U' exists2 x, x \in U & phi x = y)
total_minor_map phi
Proof.
moveH [M1 M2 M3].
apply: strict_is_minor. (omap phi). split.
- case ⇒ [y|]; last by None. case: (M1 y) ⇒ x E.
(Some x). by rewrite /= E.
- move ⇒ [y|].
+ rewrite preim_omap_None. exact: connected1.
- move ⇒ [x|] [y|] //=.
+ move/M3 ⇒ [x0] [y0] [H1 H2 H3]. (Some x0); (Some y0).
by rewrite !preim_omap_Some !mem_imset.
+ move/H ⇒ [x0] H1 H2. (Some x0); None.
rewrite !preim_omap_Some !preim_omap_None !inE !eqxx !mem_imset //.
by rewrite -mem_preim H2.
+ move/H ⇒ [y0] H1 H2. None; (Some y0).
rewrite !preim_omap_Some !preim_omap_None !inE !eqxx !mem_imset //.
by rewrite -mem_preim H2.
Qed.

Lemma minor_with (H G': sgraph) (S : {set H}) (i : H) (N : {set G'})
(phi : (sgraph.induced S) option G') :
i \notin S
( y, y \in N exists2 x , x \in phi @^-1 (Some y) & val x -- i)
@minor_map (sgraph.induced S) G' phi
Proof.
moveHi Hphi mm_phi.
pose psi (u:H) : option (add_node G' N) :=
match @idP (u \in S) with
| ReflectT pobind (fun xSome (Some x)) (phi (Sub u p))
| ReflectF _if u == i then Some None else None
end.
have psi_G' (a : G') : psi @^-1 (Some (Some a)) = val @: (phi @^-1 (Some a)).
{ apply/setPx. rewrite !inE. apply/eqP/imsetP.
+ rewrite /psi. case: {-}_ / idPp; last by case: ifP.
case E : (phi _) ⇒ [b|//] /= [<-]. (Sub x p) ⇒ //. by rewrite !inE E.
+ move ⇒ [[/= b Hb] Pb] →. rewrite /psi. case: {-}_ / idP ⇒ //= Hb'.
rewrite !inE (bool_irrelevance Hb Hb') in Pb. by rewrite (eqP Pb). }
have psi_None : psi @^-1 (Some None) = [set i].
{ apply/setPz. rewrite !inE /psi.
case: {-}_ / idP ⇒ [p|_]; last by case: ifP.
have Hz : z != i. { apply: contraNN Hi. by move/eqP <-. }
case: (phi _) ⇒ [b|]; by rewrite (negbTE Hz). }
case: mm_phiM1 M2 M3. psi;split.
- case.
+ movea. case: (M1 a) ⇒ x E. (val x). apply/eqP.
rewrite mem_preim psi_G' mem_imset //. by rewrite !inE E.
+ i. rewrite /psi. move: Hi.
case: {-}_ / idP ⇒ [? ?|_ _]; by [contrab|rewrite eqxx].
- case.
+ movey. move: (M2 y). rewrite psi_G'. exact: connected_in_subgraph.
+ rewrite psi_None. exact: connected1.
- move ⇒ [a|] [b|]; last by rewrite sg_irrefl.
+ move ⇒ /= /M3 [x0] [y0] [? ? ?].
(val x0). (val y0). by rewrite !psi_G' !mem_imset.
+ move ⇒ /= /Hphi [x0] ? ?. (val x0); i. by rewrite psi_None set11 !psi_G' !mem_imset.
+ move ⇒ /= /Hphi [x0] ? ?. i; (val x0). by rewrite sg_sym psi_None set11 !psi_G' !mem_imset.
Qed.

## Excluded-Minor Characterization of Forests

Lemma minor_rmapI (G H : sgraph) (phi : H {set G}) (f : H nat) :
injective f
( x : H, phi x != set0)
( x : H, connected (phi x))
( x y : H, f x < f y [disjoint phi x & phi y])
( x y : H, f x < f y x -- y neighbor (phi x) (phi y))
minor_rmap phi.
Proof.
moveinj_f M1 M2 M3 M4. split ⇒ // x y xy.
- wlog: x y xy / f x < f y; last exact: M3.
moveW. case: (ltngtP (f x) (f y)); first exact: W.
+ rewrite disjoint_sym eq_sym in xy ×. exact: W.
+ move/inj_fE. by rewrite E eqxx in xy.
- wlog: x y xy / f x < f y; last by moveHf; exact: M4 Hf xy.
moveW. case: (ltngtP (f x) (f y)); first exact: W.
+ rewrite neighborC sgP in xy ×. exact: W.
+ move/inj_fE. by rewrite E sgP in xy.
Qed.

Lemma non_forerst_K3 (G : sgraph) : ¬ is_forest [set: G] minor G 'K_3.
Proof.
move/is_forestP/is_forestPn ⇒ [x0] [y0] [p0] [q0] [_ _ pDq].
have [x [y] [p1] [p2] [p12_disj p1_ne]] := disjoint_part (valP p0) (valP q0) pDq.
clear x0 y0 p0 q0 pDq.
pose phi (i : 'K_3) : {set G} :=
match i with
| Ordinal 0 _[set x]
| Ordinal 1 _interior p1
| Ordinal 2 _y |: interior p2
| Ordinal _ _set0
end.
suff: minor_rmap phi by apply: minor_of_rmap.
have xDy : x != y.
{ apply: contra_neq p1_ne ⇒ ?; subst y.
by rewrite /path_of_ipath (irredxx (valP p1)) interior_idp. }
apply: minor_rmapI; first exact: ord_inj.
- case ⇒ [[|[|[|i]]] Hi] //=; [exact: set10 | exact: setU1_neq].
- case ⇒ [[|[|[|i]]] Hi] //=.
+ exact: connected1.
+ exact: connected_interior.
+ exact: connected_interiorR.
- case ⇒ [[|[|[|i]]] Hi]; case ⇒ [[|[|[|j]]] Hj] //= _.
+ by rewrite disjoints1 !inE eqxx.
+ by rewrite disjoints1 !inE eqxx (negbTE xDy).
+ rewrite disjoint_sym disjointsU // ?disjoints1 1?disjoint_sym //.
by rewrite !inE eqxx.
- case ⇒ [[|[|[|i]]] Hi]; case ⇒ [[|[|[|j]]] Hj] //= _ _.
+ apply: path_neighborL ⇒ //. by rewrite inE.
+ exact: neighbor_interiorL.
+ apply: neighborUl. rewrite neighborC.
apply: path_neighborR ⇒ //. by rewrite inE.
Qed.

Theorem K3_free_forest G : ¬ minor G 'K_3 is_forest [set: G].
Proof.
split.
- rewrite (rwP (is_forestP _)). apply: contra_notT. move/is_forestP.
exact: non_forerst_K3.
- case/forest_TW1T [B []]. exact: treewidth_K_free.
Qed.

Theorem TW1_forest G : ( T B, sdecomp T G B width B 2) is_forest [set: G].
Proof.
split ⇒ [[T] [B] [decB wB]|]; last exact: forest_TW1.
apply/K3_free_forest. exact: treewidth_K_free decB wB.
Qed.