FKS2.Table4Ext.cover_of_chainOk

theorem cover_of_chainOk (cells : List Cell) (lo : ℕ) (hne : cells ≠ [])    (hchain : chainOk lo cells = true) {x : ℝ}    (hx_lo : exp (lo : ℝ) ≤ x) (hx_hi : x ≤ exp ((lastB lo cells : ℕ) : ℝ)) :    ∃ c ∈ cells, x ∈ Set.Icc (exp (c.b : ℝ)) (exp (c.b' : ℝ)) := by  induction cells generalizing lo with  | nil => exact absurd rfl hne  | cons c rest ih =>      simp only [chainOk, Bool.and_eq_true, beq_iff_eq] at hchain      obtain ⟨hb, hrest⟩ := hchain      by_cases hsplit : x ≤ exp ((c.b' : ℕ) : ℝ)      · refine ⟨c, List.mem_cons_self .., ?_, hsplit⟩        rw [hb]        exact hx_lo      · rw [not_le] at hsplit        have hx_lo' : exp ((c.b' : ℕ) : ℝ) ≤ x := le_of_lt hsplit        have hx_hi' : x ≤ exp ((lastB c.b' rest : ℕ) : ℝ) := by          simpa only [lastB] using hx_hi        cases rest with        | nil =>            exfalso            simp only [lastB] at hx_hi'            exact absurd hx_hi' (not_le.mpr hsplit)        | cons d rest' =>            obtain ⟨e, he, hxe⟩ :=              ih c.b' (by simp) hrest hx_lo' hx_hi'            exact ⟨e, List.mem_cons_of_mem _ he, hxe⟩