def NetworkFlow.dirPathLengths {V : Type u_1} (adj : V → V → Prop) (s t : V) : Set ℕ∞

noncomputable def NetworkFlow.dirDist {V : Type u_1} (adj : V → V → Prop) (s t : V) : ℕ∞

noncomputable def NetworkFlow.residualDist {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : ℕ∞

def NetworkFlow.EdgeOnPath {V : Type u_1} (path : List V) (u v : V) : Prop

def NetworkFlow.IsShortestAugmentingPath {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (p : List V) : Prop

def NetworkFlow.IsShortestPathAugmentation {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) : Prop

theorem NetworkFlow.dirDist_le_of_path {V : Type u_1} [Fintype V] [DecidableEq V] {adj : V → V → Prop} {s t : V} {p : List V} (hp : IsDirectedPath adj s t p) : dirDist adj s t ≤ ↑(p.length - 1)

theorem NetworkFlow.isDirectedPath_take {V : Type u_1} [Fintype V] [DecidableEq V] {adj : V → V → Prop} {s t : V} {p : List V} (hp : IsDirectedPath adj s t p) (j : ℕ) (hj : 1 ≤ j) (hj2 : j + 1 ≤ p.length) : IsDirectedPath adj s (p.get ⟨j, ⋯⟩) (List.take (j + 1) p)

theorem NetworkFlow.new_edge_on_reverse_path {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) (p : List V) (hp_aug : IsAugmentingPath N fl p) (hflow_change : ∀ (u v : V), ¬EdgeOnPath p u v → ¬EdgeOnPath p v u → fl'.f u v = fl.f u v) {u v : V} (hnew : resAdj N fl' u v) (hold : ¬resAdj N fl u v) : EdgeOnPath p v u

theorem NetworkFlow.getElem_take_append_drop {V : Type u_1} [Fintype V] [DecidableEq V] {w : List V} {i j k : ℕ} (hij : i < j) (hj_lt : j < w.length) (hk : k < (List.take (i + 1) w ++ List.drop (j + 1) w).length) : (List.take (i + 1) w ++ List.drop (j + 1) w)[k] = if k ≤ i then w[k] else w[k + (j - i)]

theorem NetworkFlow.eq_of_getElem?_eq {V : Type u_1} [Fintype V] [DecidableEq V] (w : List V) (i j : ℕ) (hi : i < w.length) (hj : j < w.length) (h : w[i]? = w[j]?) : w[i] = w[j]

theorem NetworkFlow.walk_to_simple_path {V : Type u_1} [Fintype V] [DecidableEq V] {adj : V → V → Prop} {s t : V} (w : List V) (hlen : w.length ≥ 2) (hhead : w.head? = some s) (hlast : w.getLast? = some t) (hadj : ∀ (i : ℕ) (hi : i + 1 < w.length), adj (w.get ⟨i, ⋯⟩) (w.get ⟨i + 1, hi⟩)) (hst : s ≠ t) : ∃ (q : List V), IsDirectedPath adj s t q ∧ q.length ≤ w.length

theorem NetworkFlow.dirDist_ge_position_on_shortest_path {V : Type u_1} [Fintype V] [DecidableEq V] {adj : V → V → Prop} {s t : V} {p : List V} (hp : IsDirectedPath adj s t p) (hshortest : ↑(p.length - 1) = dirDist adj s t) (j : ℕ) (hj : 1 ≤ j) (hj2 : j < p.length) (hst : s ≠ t) : ↑j ≤ dirDist adj s (p.get ⟨j, hj2⟩)

theorem NetworkFlow.per_vertex_dist_bound {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) (p : List V) (hp_aug : IsAugmentingPath N fl p) (hp_shortest : ↑(p.length - 1) = residualDist N fl) (hflow_change : ∀ (u v : V), ¬EdgeOnPath p u v → ¬EdgeOnPath p v u → fl'.f u v = fl.f u v) (p' : List V) (hp' : IsDirectedPath (resAdj N fl') N.s N.t p') (j : ℕ) (hj : 1 ≤ j) (hj2 : j < p'.length) : dirDist (resAdj N fl) N.s (p'.get ⟨j, hj2⟩) ≤ ↑j

theorem NetworkFlow.new_path_length_ge_old_dist {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) (h : IsShortestPathAugmentation N fl fl') (k : ℕ) (p' : List V) (hp' : IsDirectedPath (resAdj N fl') N.s N.t p') (hlen : p'.length = k + 1) : residualDist N fl ≤ ↑k

theorem NetworkFlow.shortest_augmenting_path_monotone {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl fl' : STFlow N) (h : IsShortestPathAugmentation N fl fl') : residualDist N fl ≤ residualDist N fl'