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