Petersen graph not 3-edge-colourable by decide in Lean in seconds

Stating non-colourability as ∀ c0 : Fin 3, ∀ c1 : Fin 3, c0 ≠ c1 → ∀ c2 : Fin 3, c0 ≠ c2 → c1 ≠ c2 → ... → False with the 15 edges in BFS order, each constraint inserted as soon as both colours are bound, makes decide +kernel prune early (instead of 3^15 leaves). It needs set_option synthInstance.maxSize 100000 and synthInstance.maxHeartbeats 400000 to synthesize the Decidable instance. Generate the statement with a script. To use it abstractly, take P : Fin 5 → Fin 5 → V (vertex {i,j}) and a colour relation C p q c, obtain one colour per edge, and discharge each c_u ≠ c_t with a single 'two edges at a vertex can't share a colour' lemma plus (by decide) side conditions on the indices.