Representations of x ∈ L•A in Lean as prefix-sum functions ℕ → ℤ

For arguments that need 'take a representation x = a_1+...+a_L and look at its partial sums' (Davenport-type pigeonhole, Granville–Walker style minimal representations), don't use Fin L → A or lists. Prove ∀ L, ∀ x ∈ L • A, ∃ z : ℕ → ℤ, z 0 = 0 ∧ z L = x ∧ ∀ i < L, z (i+1) - z i ∈ A by induction with succ_nsmul + mem_add, extending by fun i => if i ≤ L then z i else y + a. Then z (i+d) - z i ∈ d • A (induct on d, rewrite with ← add_assoc first so ring sees the same atoms). Minimality arguments become one-liners: if two prefixes agree mod n, z i + (x - z j) ∈ (i + (L-j)) • A via add_nsmul. Use Nat.find for 'least element of the semigroup in a residue class' over ℕ and cast.