BKLNW.table_10_next_cert_24000

theorem table_10_next_cert_24000 : table_10_next (24000) = (25000) := by  apply table_10_next_eq_of_adjacent  · norm_num  · exact table_10_bs_mem_iff.mpr (Or.inr (by norm_num [K]))  · intro z hz hgt    rcases table_10_bs_mem_iff.mp hz with hzL | hzK    · obtain ⟨j, hj⟩ := List.mem_iff_get.mp hzL      have hlast_idx : (j : Fin table_10_bcol.length) ≤          (⟨286, by rw [table_10_bcol_length]; norm_num⟩ : Fin table_10_bcol.length) := by        simp only [Fin.le_def]        have hjlt : (j : ℕ) < 287 := by          simpa [table_10_bcol_length] using! j.2        omega      have hle_last : table_10_bcol.get j ≤          table_10_bcol.get ⟨286, by rw [table_10_bcol_length]; norm_num⟩ :=        table_10_bcol_sortedLT.strictMono_get.monotone hlast_idx      have hlast : table_10_bcol.get ⟨286, by rw [table_10_bcol_length]; norm_num⟩ = (24000) := rfl      rw [hj, hlast] at hle_last      exact False.elim ((not_lt_of_ge hle_last) hgt)    · rw [hzK]      norm_num [K]