Equitable Vizing colourings on a prescribed palette

A finite simple graph has an equitable proper edge colouring on any palette of at least maxDegree + 1 colours. Unused colours are included in the balancing, and every class has at most the ceiling of the average size.

theorem LeanPool.Vizing.exists_equitable_edge_colouring {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ℕ) (hc : G.maxDegree + 1 ≤ c) : ∃ (colour : Sym2 V → Fin c), ColourClasses.ProperOn G.edgeFinset colour ∧ EquitableDefinitions.IsEquitable G.edgeFinset colour ∧ ∀ (a : Fin c), (ColourClasses.colourClass G.edgeFinset colour a).card ≤ EquitableDefinitions.classCeiling G.edgeFinset.card c

Every palette of at least maxDegree + 1 colours admits an equitable proper edge colouring, with each class bounded by the ceiling average.