Subcubic Brooks theorem: Greedy

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

theorem BrooksSubcubic.greedy_coloring_zero {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) (hk : 0 < k) (rank : V → ℕ) (hrank : Function.Injective rank) (h : ∀ (v : V), {w ∈ G.neighborFinset v | rank w < rank v}.card < k) : ∃ (c : V → Fin k), (∀ (u v : V), G.Adj u v → c u ≠ c v) ∧ ∀ (v : V), {w ∈ G.neighborFinset v | rank w < rank v}.card = 0 → c v = ⟨0, hk⟩

Greedy colouring picking the LEAST unused colour, with control: a vertex whose set of strictly-lower-ranked neighbours is empty receives colour 0.