Subcubic Brooks theorem: K4Free

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

theorem BrooksSubcubic.exists_nonadj_pair_of_cubic_K4free {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hK4 : G.CliqueFree 4) {v₀ : V} (hdeg : G.degree v₀ = 3) : ∃ (a : V) (b : V), G.Adj v₀ a ∧ G.Adj v₀ b ∧ a ≠ b ∧ ¬G.Adj a b

In a K₄-free graph, a degree-3 vertex has two non-adjacent neighbours.