firstReturn_pos — Mathlib

English

If p is nonempty, then p.firstReturn is greater than zero.

Русский

Если p непусто, то p.firstReturn > 0.

LaTeX

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

Lean4

theorem firstReturn_pos : 0 < p.firstReturn :=
  by
  rw [← not_le, Nat.le_zero, firstReturn, findIdx_eq, getElem_range]
  · simp only [not_lt_zero', IsEmpty.forall_iff]
    rw [← p.cons_tail_dropLast_concat h]
    simp
  · rw [length_range, length_pos_iff]
    exact toList_ne_nil.mpr h

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