Subcubic Brooks theorem: Endblock

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

theorem BrooksSubcubic.good_triple_of_two_cut {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hreg : ∀ (v : V), G.degree v = 3) (hnocut : ∀ (z : V), (SimpleGraph.induce {z}ᶜ G).Connected) (a₀ y w : V) (hay : a₀ ≠ y) (hw : w ∉ {a₀, y}) (hcut : ¬(SimpleGraph.induce {a₀, y}ᶜ 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

Lovász's endblock case: in a cubic graph with no cut vertex, if some pair {a₀,y} separates the graph, an end component supplies a good triple.