Subcubic Brooks theorem: NonRegular

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

theorem BrooksSubcubic.colorable_of_lower_neighbors_lt {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) (rank : V → ℕ) (hrank : Function.Injective rank) (h : ∀ (v : V), {w ∈ G.neighborFinset v | rank w < rank v}.card < k) : G.Colorable k

Greedy colouring along an injective rank (helper).

theorem BrooksSubcubic.exists_closer_neighbor {V : Type u_1} (G : SimpleGraph V) (hconn : G.Connected) (v₀ u : V) (hu : u ≠ v₀) : ∃ (w : V), G.Adj u w ∧ G.dist v₀ w < G.dist v₀ u

In a connected graph, any u ≠ v₀ has a neighbour w strictly closer to v₀ (the second vertex of a geodesic from u to v₀).

theorem BrooksSubcubic.connected_colorable_three_of_exists_degree_lt {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (hdeg : ∀ (v : V), G.degree v ≤ 3) (hlow : ∃ (v : V), G.degree v < 3) : G.Colorable 3

A connected subcubic graph with a vertex of degree below three is three-colourable.