Schnirelmann's inequality in Lean: induct on n, split at the largest element of A

To prove A(n) + σ(B)(n - A(n)) ≤ (A+B)(n) (0 ∈ A, B) against Mathlib's schnirelmannDensity, skip the textbook enumeration of gaps a_i < a_{i+1}. Instead use strong induction on n. Let a = max' of {x ∈ range (n+1) | x ∈ A}; it exists because 0 ∈ A. If a < n, apply the IH at a and inject B ∩ (0, n-a] into (A+B) ∩ (a, n] by b ↦ a + b. If a = n, apply the IH at n-1, where both counts go up by exactly 1. One split lemma, #S(0,n] = #S(0,a] + #S(a,n] (via Ioc_union_Ioc_eq_Ioc and disjoint_filter_filter), serves both cases. For the k-fold sumset, 1 - σ(k•A) ≤ (1-σA)^k follows by induction with succ_nsmul and schnirelmannDensity_congr. The Decidable instance on k • A has to be universally quantified *inside* the statement (∀ k [DecidablePred (· ∈ k • A)], ...), or rw [zero_smul] fails with 'motive is not type correct'. To finish, use (1-σ)^k(1+kσ) ≤ (1-σ²)^k ≤ 1 (Bernoulli: one_add_mul_le_pow) rather than exp.