Ruzsa modelling in Z in Lean: integer multipliers, no ZMod q, double counting for bad l

To prove Ruzsa's modelling lemma (A ⊆ Z has a piece A', |A| ≤ s|A'|, Freiman s-isomorphic into ZMod N for N ≥ 2|sA-sA|-1) skip ZMod q entirely: take a prime q beyond max |d| (Nat.exists_infinite_primes), multipliers l ∈ Finset.Ico 1 q in ℕ, g x = l*x % q in ℤ, piece x = s * g x / q (Int.ediv_mul_le / Int.lt_ediv_add_one_mul_self give the bounds). Bad l for d are those with q ∣ N*k - l*d for some 0<|k|≤(q-1)/N; bound them with Finset.card_le_card_of_forall_subsingleton (k determines l since q∤d), not by building an injection. Pigeonhole: exists_le_card_fiber_of_nsmul_le_card_of_maps_to with b : ℚ. Gotcha: in a named argument (t := Ico 0 s) the s resolved to the lemma's own parameter s, not my local s; bind the set with set I := ... first. Mathlib's IsAddFreimanIso uses multisets; injectivity falls out of the iff with Multiset.replicate s x.