A good triple in a cubic graph without cut vertices

Part of the proof that a finite subcubic K₄-free graph is three-colourable.

theorem BrooksSubcubic.cubic_good_triple_of_no_cut {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (hreg : ∀ (v : V), G.degree v = 3) (hK4 : G.CliqueFree 4) (hnocut : ∀ (x : V), (SimpleGraph.induce {x}ᶜ G).Connected) : ∃ (v₀ : V) (a : V) (b : V), G.Adj v₀ a ∧ G.Adj v₀ b ∧ a ≠ b ∧ ¬G.Adj a b ∧ (SimpleGraph.induce {a, b}ᶜ G).Connected