simp at *
case cons.nil
b a x : ℕ
hl_mono : List.Chain (fun u v => u < v) a [x]
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a [x]
hl_cons : [x] ≠ []
hb : b < List.getLast [x] hl_cons
n : ℕ
hn : n ∈ Set.Icc a b
⊢ ∃ lᵢ, lᵢ ∈ [x] ∧ lᵢ ∈ Set.Ioc n (2 * n)
case cons.nil
b a x : ℕ
hl_cons : [x] ≠ []
hb : b < x
n : ℕ
hl_mono : a < x
hl_slow : x ≤ 2 * a
hn : a ≤ n ∧ n ≤ b
⊢ n < x ∧ x ≤ 2 * n