feat(Combinatorics/SimpleGraph): If a graph has a Walk starting and ending in the same vertex then the chromatic number is grater than two

[IvanRenison]

---

The theorem is named Walk.two_lt_chromaticNumber_of_odd_closed, but I'm not sure if that is the best name. I didn't use the word cycle because in Connectivity.lean a cycle is defined as a Walk that start and ends in the same vertex and has no other repeated vertex, so it's not what I'm using here.