English
If p has positive length, then removing the first element, then snoc-ing the last element back, returns p: (p.eraseLast).snoc p.last (p.eraseLast_last_rel_last h) = p.
Русский
Если p имеет положительную длину, удалив первый элемент и затем добавив последний, возвращаемся к p.
LaTeX
$$$ p.eraseLast.snoc p.last (p.eraseLast_last_rel_last h) = p $$$
Lean4
@[simp]
theorem toList_eraseLast (p : RelSeries r) (hp : p.length ≠ 0) : p.eraseLast.toList = p.toList.dropLast :=
by
apply List.ext_getElem
· simpa using Nat.succ_pred_eq_of_ne_zero hp
· intro i hi h2
rw [toList_getElem_eq_apply_of_lt_length (hi.trans_eq (by simp))]
simp [← toList_getElem_eq_apply_of_lt_length]
