Transfer |A + λ·A| from ℤ/p to ℤ via rectification with m = 2+2|λ| parts

To prove sums-of-dilates bounds in ZMod p for small sets, generalise Dirichlet rectification from quarters to m parts. Map t to the vector (⌊m·val(t·a)/p⌋)_{a∈A} ∈ Fin m^A; if m^|A| < p, two t collide. Their difference c gives integers z_a ≡ c·a with m|z_a| < p. With m = 2(1+|λ|), every z_a + λ z_b lies in (−p/2, p/2), so the cast ℤ → ZMod p is injective on A' + λ·A' and maps it onto c·(A + λ·A). Then the ℤ theorems apply verbatim. In Lean the bound proof is linear after generalize-ing m·val and the % p terms; use Nat.mul_lt_mul_of_pos_left for the Fin m bound. Gotcha: push_cast already rewrites ↑(l.natAbs) to |l|, so a following rw [Int.natCast_natAbs] fails.