Coloring odd loops / components

Stream: graph theory

[John Talbot]

Is this in Mathlib?

G.Colorable 2 ↔ ∀ u, ∀ (w : G.Walk u u), ¬ Odd w.length

I can see Walk.three_le_chromaticNumber_of_odd_loop but the other direction would seem to require something like

G.Colorable n ↔ ∀ c : G.ConnectedComponent, (G.induce c).Colorable n

which I also can't see.

Am I missing something obvious? (If not I'd be happy to add these.)