Proving Menger's Theorem (edge version) using mincut maxflow

Question

I know this is a classic that has been discussed here on stackexchange plenty of times. However I think my question is specific enough and addresses a often neglected point so that I feel like this question is sufficiently different from the others to justify a new thread.

Okay so here's a typical proof of the edge version of Menger based on Mincut-Maxflow: (source: http://web.math.ucsb.edu/~padraic/mathcamp_2011/flows_graphs/MC2011_flows_graphs_wk2_day2.pdf)

2 Menger’s Theorem

We now continue with a classical theorem of Menger:

Theorem 3

Let s, t be a pair of distinct vertices in an undirected graph G. Then, the minimal number of edges needed to separate2 s from t is equal to the maximal number of edge-disjoint paths connecting s to t.

Proof. Let s, t be the source and sink nodes of G, respectively, replace each of G’s undirected edges {x, y} with pairs of edges (x, y),(y, x), and let c be a capacity function on G that assigns 1 to every edge. Let f be a maximal flow on G, and S be a corresponding minimal cut. Our flow f clearly defines the maximal number of edge-disjoint paths from s to t, by identifying edges as being in a path iff f is 1 on them. Similarly, S clearly corresponds to a minimal separating set of edges; therefore, because the value of any maximum flow is the value of a minimal cut, we’ve completed our proof. End of article

However I feel that this proof, like so many others glosses over what I think is the trickiest part: namely, that the value of the maximum flow is equal to the max number of edge-disjoint paths.It says "Our flow f clearly defines the maximal number of edge-disjoint paths from s to t, by identifying edges as being in a path iff f is 1 on them." But I think this only proves rigorously that $|f| \geq k$ for $|f|$ the value of the flow $k$ the max number of edge disjoint paths. How do you prove rigorously that $|f|\leq k $? A.k.a. that given a set $P, |P|= k$ of maximum number of edge disjoint paths, you can't find a flow of value strictly greater than $k$ (given that the capacities are $1$ in each edge and f is integer valued, aka $1$ or $0$ on each edge.)

Answer 1

I know this is long overdue, but here's my explanation of why this works. Say that the value of the max flow is $|f|$, then since all edges have capacity $1$ there are $|f|$ edges in the cut (since from the max-flow min-cut theorem the max flow value is equal to the flow over the cut). Now assume that there are more than $|f|$ edge-disjoint paths, then they will share an edge in the cut, this is a contradiction with them being edge-disjoint. Now assume that there are less than $|f|$ edge-disjoint paths, then since the capacity of each edge is $1$ there will be at least one edge with flow $0$ in the cut, but that's also a contradiction.

Answer 2

It is sufficient to prove the following:

Given a $s-t$ $0-1$ flow of size $k$, there exists $k$ edge-disjoint paths from $s$ to $t$ within the set of all the edges that have flow $1$.

Use induction on the size of this set and $k$.
The idea is to keep following an edge with flow $1$ (must exist at intermediate nodes by flow conservation), until we reach $t$, or cycle back to a vertex already visited.

In both of these cases, we can zero out the flow (along the $s-t$ path or the cycle) and use the induction hypothesis.

The details are not too hard!