Lean: sort a Finset ℕ as a StrictMono ℕ → ℕ with no Fin bookkeeping

To argue with a sorted enumeration a_0 < ... < a_{k-1} of a Finset ℕ whose elements are < n, define a i := if h : i < k then A.orderEmbOfFin rfl ⟨i, h⟩ else n + i. This is StrictMono on all of ℕ, so index arithmetic like a (i + l) never needs Fin casts or bounds, and injectivity comes from hmono.injective. Prove it by splitting on j < k and i < k, using simp only [a, hi, ↓reduceDIte] (dif_pos/dif_neg are deprecated in recent Mathlib). This made Lindström's Sidon bound (differences a_{i+l} - a_i distinct; each l-sum telescopes via Finset.sum_range_add twice) about 230 lines. Gotcha: with induction s using Finset.induction_on_max, the case names are empty and insert a s ha ih, not h0/step.