proposition: Lemma K4_of_vseparators (G : sgraph) : 3 < #|G| -> (forall S : {set G}, vseparator S -> 2 < #|S|) -> minor G K4.
proof: Proof. move => G4elt minsep3. case: (boolP (cliqueb [set: G])) => [|/cliquePn [x] [y] [_ _ xNy xNEy]]. { move/cliqueP. apply: minor_of_clique. by rewrite cardsT. } have minsep_xy S : separates x y S -> 3 <= #|S|. { move => A. apply: minsep3. by exists x; exists y. } case: (theta xNEy xNy minsep_xy) => p ind_p. case: (theta_vertices p xNy xNEy) => s Hs. pose p1 := p ord1. pose p2 := p ord2. pose s1 := s ord1. pose s2 := s ord2. have ind12 : independent p1 p2 by apply: ind_p. have ind01 : independent (p ord0) p1 by apply: ind_p. have ind02 : independent (p ord0) p2 by apply: ind_p. have sp1 : s1 \in interior p1 by rewrite Hs. have sp2 : s2 \in interior p2 by rewrite Hs. case (@avoid_nonseperator G [set x; y] (s ord0) (s1)) => //; try (apply: interiorN; eauto). { move/minsep3. by rewrite cards2 xNy. } move => q Iq av_xy. case: (@split_at_first G [predU interior p1 & interior p2] (s ord0) s1 q s1) => //. { by rewrite inE /= sp1. } move => s1' [q1 [q2 [catp s1'p12 s1'firstp12]]]. subst q. case/irred_catE : Iq => Iq _ _. have {av_xy} av_xy : [disjoint q1 & [set x; y]] by apply/disjointP => z; set_tac. wlog in_p1: p1 p2 s1 s2 ind01 ind02 ind12 sp1 {sp2} {q2 s1'p12} s1'firstp12 / s1' \in interior p1. { move => W. case/orP: (s1'p12) => /= [s1'p1|s1'p2]. - by apply W with p1 p2 s1. - apply W with p2 p1 s2 => //. by apply: independent_sym. move => z' H1 H2. apply s1'firstp12 => //. move: H1. by rewrite !inE orbC. } apply K4_of_paths with x y (s ord0) s1' (p ord0) p1 p2 q1 => //; exact: valP. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)