theorem NetworkFlow.isMaxFlow_of_noAugmentingPath {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hmax : NoAugmentingPath N fl) : IsMaxFlow N fl

def NetworkFlow.IsPathEdge {V : Type u_1} (l : List V) (u v : V) : Prop

theorem NetworkFlow.general_path_augment {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (l : List V) (hne : l ≠ []) (hchain : List.IsChain (resAdj' N fl) l) (hnodup : l.Nodup) (hlen : l.length ≥ 2) (hhead : l.head hne = N.s) (hlast : l.getLast hne = N.t) : ∃ (fl' : STFlow N), flowValue N fl < flowValue N fl'

theorem NetworkFlow.multi_hop_augment {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (htrans : Relation.TransGen (resAdj' N fl) N.s N.t) (c : V) (hsc : resAdj' N fl N.s c) (hne : c ≠ N.t) (hct : Relation.ReflTransGen (resAdj' N fl) c N.t) (d : V) (hsd : Relation.ReflTransGen (resAdj' N fl) N.s d) (hdt : resAdj' N fl d N.t) (hds : d ≠ N.s) : ∃ (fl' : STFlow N), flowValue N fl < flowValue N fl'

theorem NetworkFlow.augment_along_residual_path {V : Type u_2} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hreach : ResReachable N fl N.t) : ∃ (fl' : STFlow N), flowValue N fl < flowValue N fl'

theorem NetworkFlow.exists_better_flow_of_resReachable {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) (hreach : ResReachable N fl N.t) : ∃ (fl' : STFlow N), flowValue N fl < flowValue N fl'

theorem NetworkFlow.isMaxFlow_iff_noAugmentingPath {V : Type u_1} [Fintype V] [DecidableEq V] (N : FlowNetwork V) (fl : STFlow N) : IsMaxFlow N fl ↔ NoAugmentingPath N fl