English
For any j < n, there exists i with j < sizeUpTo(i+1) and i < length.
Русский
Для любого j < n существует i с j < sizeUpTo(i+1) и i < length.
LaTeX
$$$\\exists i < c.length \\; (j < c.sizeUpTo(i+1))$$$
Lean4
/-- `index_exists` asserts there is some `i` with `j < c.sizeUpTo (i+1)`.
In the next definition `index` we use `Nat.find` to produce the minimal such index.
-/
theorem index_exists {j : ℕ} (h : j < n) : ∃ i : ℕ, j < c.sizeUpTo (i + 1) ∧ i < c.length :=
by
have n_pos : 0 < n := lt_of_le_of_lt (zero_le j) h
have : 0 < c.blocks.sum := by rwa [← c.blocks_sum] at n_pos
have length_pos : 0 < c.blocks.length := length_pos_of_sum_pos (blocks c) this
refine ⟨c.length - 1, ?_, Nat.pred_lt (ne_of_gt length_pos)⟩
have : c.length - 1 + 1 = c.length := Nat.succ_pred_eq_of_pos length_pos
simp [this, h]
