Split a vertex list at a consecutive pair
ProvedEdmondsKarp.ShortestPath.pathArcs_splitgraph-theorynetwork-flow
If an ordered pair occurs as a consecutive arc of a vertex list, the list decomposes into a prefix, those two vertices, and a suffix.
Preamble
import Definitions.Def_EdmondsKarp_ShortestPath_Run open EdmondsKarp.ShortestPath
Formal statement
theorem EdmondsKarp.ShortestPath.pathArcs_split {V : Type} [Fintype V] [DecidableEq V] (P : List V)
(u v : V) (h : (u, v) ∈ pathArcs P) : ∃ L R, P = L ++ u :: v :: R := by sorrySource
Edmonds and Karp (1972), §1.2 pp. 251–252, residual shortest-path distance and simple-path bounds. DOI: 10.1145/321694.321699.