English
A variant induction principle: to prove a property for all RelSeries, it suffices to prove it for singletons and show that if it holds for a series p, then it holds for p.snoc x hx; this mirrors induction on length but by a slightly different construction.
Русский
Вариант индукции: чтобы доказать свойство для всех RelSeries, достаточно доказать для одиночных, и показать, что если свойство верно для p, то верно и для p.snoc x hx.
LaTeX
$$Induction principle with tail and snoc step: ...$$
Lean4
theorem snoc_self_eraseLast (p : RelSeries r) (h : p.length ≠ 0) :
p.eraseLast.snoc p.last (p.eraseLast_last_rel_last h) = p :=
by
apply toList_injective
rw [toList_snoc, ← getLast_toList, toList_eraseLast _ h, List.dropLast_append_getLast]
