WalkCycle.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Convert the standard library's cycle walks into exact cycle witnesses.

theorem OAI.CycleClique.Construction.hasCycle_of_isCycle line 11
theorem OAI.CycleClique.Construction.hasCycle_of_path_close line 28
Source documentation
A simple path of at least two edges closes to an exact cycle when its endpoints are adjacent. This is the single-chain case of path closure.
```
theorem hasCycle_of_path_close {x y : V} {p : G.Walk x y}
    (hp : p.IsPath) (hlen : 2 ≤ p.length) (hclose : G.Adj y x) :
    HasCycle G (p.length + 1) := by
…
```
Mentions: OAI.CycleClique.Construction.HasCycle