Subcubic Brooks theorem: Main

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

theorem BrooksSubcubic.brooks_cubic {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hΔ : G.maxDegree ≤ 3) (hK4 : G.CliqueFree 4) : G.Colorable 3

Brooks' theorem for subcubic graphs: a finite simple graph with maximum degree ≤ 3 and no 4-clique is 3-colourable.