noncomputable def NetworkFlow.resCap {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (u v : V) : ℝ

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

theorem NetworkFlow.resCap_nonneg {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (u v : V) : 0 ≤ resCap N fl u v

theorem NetworkFlow.resAdj_iff {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (u v : V) : resAdj N fl u v ↔ N.cap u v - fl.f u v > 0 ∨ fl.f v u > 0

def NetworkFlow.IsDirectedPath {V : Type u_1} (adj : V → V → Prop) (s t : V) (p : List V) : Prop

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

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

theorem NetworkFlow.augmentingPath_iff_residualPath' {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (p : List V) : IsOriginalAugmentingPath N fl p ↔ IsDirectedPath (resAdj N fl) N.s N.t p

noncomputable def NetworkFlow.pathBottleneck {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (p : List V) (hp : p.length ≥ 2) : ℝ