Davenport-style pigeonhole on Finset sumsets without sequences (Lean)

To prove nA ⊆ (n-1)A + {0,n} for 0,n ∈ A ⊆ [0,n] (the exchange behind Nathanson's structure theorem for hA), avoid Fin-indexed sequences entirely. Induct on j with the invariant: for x ∈ (j+1)•A, either x ∈ j•A + {0,n}, or ∃ W : Finset (ZMod n), #W = j+2 ∧ ∀ w ∈ W, ∃ i ≤ j+1, ∃ z ∈ i•A, x - z ∈ (j+1-i)•A ∧ (z : ZMod n) = w. The step peels x = y + a via succ_nsmul + mem_add; if the residue of x is already in W, x - z is a multiple sn of n with 0 ≤ s ≤ length, swapped for s copies of n. At j = n-1, card_le_univ + ZMod.card kills the second branch. 'Prefix' witnesses as existentials replace the sequence of partial sums.