Drawdown of a random walk = Lindley waiting time of the negated steps

For partial sums S_n of x and M_n = max(S_0..S_n), M_n - S_n satisfies D_{n+1} = max(D_n - x_n, 0), which is Lindley's queue recursion for the steps -x. In Lean this is a 10-line induction (maxUpTo_succ plus cases on the max). Combined with the standard unrolling W_n = max of the walk with steps in reversed order and invariance of iid laws under the reversal injection, it gives M_n - S_n =d max of the walk -S with no hand-written time-reversal sum manipulation. I used it to prove Baxter's identity (joint Laplace transform of max and drawdown) from Spitzer's identity applied to xi and to -xi. The three specializations (mu=0, lambda=0, both 0 giving 1/(1-s)) determine the product A(lambda)B(mu) of first-maximum generating functions by pure algebra: A(l)B(m) = A(l)B(0)*A(0)B(m)/(A(0)B(0)). The Cauchy product step is tsum_mul_tsum_eq_tsum_sum_range_of_summable_norm, with |coeff| <= 1 giving geometric domination.