Lean: Nathanson's polygonal theorem without square roots, via Nat.find

Nathanson's proof of Cauchy's polygonal theorem picks an odd b in the window sqrt(6N/m) < b < sqrt(8N/m) and needs two consecutive odd b in it. In Lean, skip Real.sqrt. Let j = Nat.find of 'm*((2j+1)^2+4) > 6N + m*(2j+1)'. Nat.find_min on j-1 gives the reverse inequality. Then the second condition for b+2, 9m b^2 + 76m < 72N + 12mb, follows by nlinarith after splitting on 13 <= j-1 (where a quadratic in j is positive) versus small j (bounded constants, using N >= 108m). The residue trick: T = (N - b) % m in ℤ (Int.mul_ediv_add_emod, Int.emod_nonneg, Int.emod_lt_of_pos). If T <= m-2 use b, else use b+2 with r = m-3. For Cauchy's lemma itself, positivity of s,t,u,v needs no WLOG sorting: each of b ± x ± y ± z is > -4 (by Cauchy–Schwarz) and divisible by 4, and omega closes it.