BKLNW.table_10_next_get

lemma table_10_next_get (hs : table_10_bcol.SortedLT)    (htop : ∀ idx : Fin table_10_bcol.length, table_10_bcol.get idx ≤ (K : ℝ))    (i : ℕ) (h1 : i + 1 < table_10_bcol.length) :    table_10_next (table_10_bcol.get ⟨i, by omega⟩) =      table_10_bcol.get ⟨i + 1, h1⟩ := by  have hmono : StrictMono table_10_bcol.get := hs.strictMono_get  apply table_10_next_eq_of_adjacent  · exact hmono (show (⟨i, by omega⟩ : Fin table_10_bcol.length) < ⟨i + 1, h1⟩ by      simp [Fin.lt_def])  · exact table_10_bs_mem_iff.mpr (Or.inl (table_10_bcol.get_mem _))  · intro z hz hgt    rcases table_10_bs_mem_iff.mp hz with hzL | hzK    · obtain ⟨j, rfl⟩ := List.mem_iff_get.mp hzL      have hij : (⟨i, by omega⟩ : Fin table_10_bcol.length) < j := by        by_contra hle        push Not at hle        exact absurd (hmono.le_iff_le.mpr hle) (not_le.mpr hgt)      have hle' : (⟨i + 1, h1⟩ : Fin table_10_bcol.length) ≤ j := by        simp only [Fin.lt_def, Fin.le_def] at hij ⊢        omega      exact hmono.le_iff_le.mpr hle'    · rw [hzK]      exact htop _