English
If p.length = coheight(p.head), then coheight(p(i)) = i.rev.
Русский
Если p.length = coheight(p.head), тогда coheight(p(i)) = i.rev.
LaTeX
$$$p.length = \operatorname{coheight}(\mathrm{head}(p)) \Rightarrow \operatorname{coheight}(p(i)) = i^{\mathrm{rev}}.$$$
Lean4
/-- In a maximally long series, i.e one as long as the coheight of the first element, the coheight of
each element is its reverse index in the series.
-/
theorem coheight_eq_index_of_length_eq_head_coheight {p : LTSeries α} (h : p.length = coheight p.head)
(i : Fin (p.length + 1)) : coheight (p i) = i.rev := by
simpa using height_eq_index_of_length_eq_height_last (α := αᵒᵈ) (p := p.reverse) (by simpa) i.rev