contradiction
case nil
a b : ℕ
hl_mono : List.Chain (fun u v => u < v) a []
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a []
hl_cons : [] ≠ []
hb : b < List.getLast [] hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ [] ∧ lᵢ ∈ Set.Ioc n (2 * n)
no goals