English
Tail removes the first element, producing a RelSeries of length one less: tail(p) has length p.length - 1, and the rest is the tail of p.
Русский
Tail удаляет первый элемент, образуя RelSeries длиной на единицу меньшей: tail(p) имеет длину p.length - 1, а остальное — часть хвоста.
LaTeX
$$$\text{length}(\text{tail}(p)) = p.length - 1$$$
Lean4
/-- If a series `a₀ -r→ a₁ -r→ ...` has positive length, then `a₁ -r→ ...` is another series
-/
@[simps]
def tail (p : RelSeries r) (len_pos : p.length ≠ 0) : RelSeries r
where
length := p.length - 1
toFun := Fin.tail p ∘ (Fin.cast <| Nat.succ_pred_eq_of_pos <| Nat.pos_of_ne_zero len_pos)
step i := p.step ⟨i.1 + 1, Nat.lt_pred_iff.mp i.2⟩
