def SimpleGraph.IsInAlternatingForest {V : Type u_1} (G : SimpleGraph V) (M : G.Subgraph) (A : Set V) (b : V) : Prop

theorem SimpleGraph.Walk.IsAugmentingPath.odd_length {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {M : G.Subgraph} (haug : p.IsAugmentingPath M) : Odd p.edges.length

theorem SimpleGraph.Walk.IsAlternatingFrom.reverse_of_odd {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {M : G.Subgraph} (halt : p.IsAlternatingFrom M) (hodd : Odd p.edges.length) : p.reverse.IsAlternatingFrom M

theorem SimpleGraph.Walk.IsAugmentingPath.reverse' {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {u v : V} {p : G.Walk u v} {M : G.Subgraph} (haug : p.IsAugmentingPath M) : p.reverse.IsAugmentingPath M

theorem SimpleGraph.walk_endpoint_parity {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {A B : Set V} (hbip : G.IsBipartiteWith A B) {u v : V} (p : G.Walk u v) : (u ∈ A → (Even p.edges.length → v ∈ A) ∧ (Odd p.edges.length → v ∈ B)) ∧ (u ∈ B → (Even p.edges.length → v ∈ B) ∧ (Odd p.edges.length → v ∈ A))

theorem SimpleGraph.augmenting_to_forest {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {A B : Set V} (hbip : G.IsBipartiteWith A B) {M : G.Subgraph} (haug : G.HasAugmentingPath M) : ∃ b ∈ B, b ∉ M.verts ∧ G.IsInAlternatingForest M A b

theorem SimpleGraph.forest_to_augmenting {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {A B : Set V} (hbip : G.IsBipartiteWith A B) {M : G.Subgraph} {b : V} (hb : b ∈ B) (hbM : b ∉ M.verts) (hforest : G.IsInAlternatingForest M A b) : G.HasAugmentingPath M

theorem SimpleGraph.forest_characterization {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} (M : G.Subgraph) (hM : M.IsMatching) (hMfin : M.edgeSet.Finite) (A B : Set V) (hbip : G.IsBipartiteWith A B) : M.IsMaxMatching ↔ ∀ b ∈ B, b ∉ M.verts → ¬G.IsInAlternatingForest M A b