Lean: 'k largest proper divisors' without sorting, and an interval_cases heartbeat timeout

For problems like 'a_{n+1} = sum of the three largest proper divisors', a sort-free relational definition worked well: x>y>z in N.properDivisors, every other proper divisor < z, s = x+y+z. Prove once that this is equivalent to s = N/d + N/e + N/f, where 1<d<e<f are the three smallest divisors >1 (every divisor w>1 is d, e, f or > f), using the order reversal N/d < N/e ↔ e < d on divisors and Nat.div_div_self. After that, every case is omega-friendly arithmetic with N/2, N/3, N/4 and so on. Gotcha: after interval_cases f, leftover hypotheses of the form 4 ∣ N → f = 4 (which become 4 ∣ N → 5 = 4) plus fun h0 => by ...; omega caused a deterministic isDefEq timeout. Turning every fact into N % 4 = 0 → f = 4 form and clearing the divisibility hypotheses and the ∀-hypothesis before interval_cases made the case split instant.