Girth and Diameter Proof

Stream: graph theory

[Kiril Vinogradov]

Hi all, I'm planning on over the next few months to slowly tackle the formalization of the attached proof
diam.webp
[The proof that the girth of a graph is less than or equal to twice its diameter + 1]
I wanted to seek some advice from more experienced Lean users as to what are your thoughts on the best way to tackle this in regards to what type of object could be best suited for this problem. Would it be best to begin the implementation of it using a cycle graph, or by ways of using a cyclic subgraph, or moreover simply by defining it as a walk that starts and ends at the same vertex and then going from there? I appreciate any advice or thoughts on this matter.

[Daniel Weber]

I think it will be easiest to use docs#SimpleGraph.Walk.IsCycle