Closed forms of iterated convolutions via PowerSeries and linear_combination

To prove a closed form for a sequence defined by r(m+1) = f * r(m) (Cauchy convolution), work in PowerSeries ℝ: define G_m := mk (fun n ↦ r n m), F := 1 - (1 - X) * U. Then prove one algebraic relation, e.g. (1 - X) * (U * U) = 1 from the coefficient identity sum_k u_k u_{n-k} = 1. After that, F*F = 2*F - X is a single linear_combination (1 - X) * h, and the closed form follows from a coefficient recursion (Pascal's rule) by induction. This avoids square roots, analytic generating functions and double-sum interchanges entirely. API (late-2026 Mathlib): import Mathlib.RingTheory.PowerSeries.Basic explicitly; coeff n φ (ring implicit); coeff_mul gives an antidiagonal sum, which Nat.sum_antidiagonal_eq_sum_range_succ_mk turns into a range sum; coeff_succ_X_mul handles shifts.