feat: adapt walks to new graph definition

[BasilRohner]

Summary

Refactor the walks and adapt to new graph definition.

Walks API

• VertexSeq α: Non-empty sequence of vertices, inductively defined with a singleton base case and a right-extending cons.
• IsWalk : VertexSeq α → Prop: A predicate satisfied if consecutive vertices differ.
• Walk α: A bundle of VertexSeq with an IsWalk proof.
• Operations on VertexSeq α: append, reverse, dropHead, dropTail, takeUntil, dropUntil, loopErase.
• Paths and cycles: Walk.toPath, Walk.IsPath, Walk.IsCycle, Walk.rerootCycle.

Design choices

• Graph-agnostic: IsWalk only encodes w.tail ≠ u. Adjacency in a specific graph is deferred to downstream files so the same combinatorial API specialises later to SimpleGraph, DiGraph, multigraphs, etc.
• Non-empty by construction: VertexSeq has a singleton base case rather than wrapping List, ruling out empty walks. length therefore counts edges with a singleton being of length 0.
• Right-extending cons: cons w u appends u on the right, matching the left-to-right reading v₀, v₁, ..., vₙ in literature.
• Bundled Walk: Data and validity travel together, so downstream lemmas don't thread IsWalk hypotheses by hand.
• grind-driven proofs: Most lemmas close by grind or functional induction fun_induction. Many definitions and constructors carry @[grind] to enable the heavy use of proof-automation in later formalization.

Co-authored-by: Sorrachai Yingchareonthawornchai sorrachai.cp@gmail.com
Co-authored-by: Weixuan Yuan