firstReturn_lt_length — Mathlib

English

If p is nonempty, then firstReturn(p) is strictly less than the length of p.toList.

Русский

Если p непусто, то firstReturn(p) строго меньше длины p.toList.

LaTeX

$$$$ p \neq 0 \implies p.firstReturn < p.toList.length. $$$$

Lean4

theorem firstReturn_lt_length : p.firstReturn < p.toList.length :=
  by
  have lp := length_pos_of_ne_nil (toList_ne_nil.mpr h)
  rw [← length_range (n := p.toList.length)]
  apply findIdx_lt_length_of_exists
  simp only [mem_range, decide_eq_true_eq]
  use p.toList.length - 1
  exact ⟨by cutsat, by rw [Nat.sub_add_cancel lp, take_of_length_le (le_refl _), p.count_U_eq_count_D]⟩

Похожие утверждения