English
For any l1, l2 with l1 a sublist of l2 and l1 IsChain under ≠, the length of l1 is at most the length of l2.destutter with respect to ≠.
Русский
Для любых l1, l2 с l1 является подпоследовательностью l2 и l1 образует ≠-цепочку, длина l1 не превосходит длины l2.destutter(≠).
LaTeX
$$$l_1 \\text{ Sublist } l_2 \\wedge l_1.IsChain(\\neq) \\Rightarrow |l_1| \\le |\\mathrm{destutter}_{\\neq}(l_2)|$$$
Lean4
/-- `destutter` of `≠` gives a list of maximal length over any chain.
In other words, `l.destutter (· ≠ ·)` is a `≠`-chain sublist of `l`, and is at least as long as any
other `≠`-chain sublist. -/
theorem length_le_length_destutter_ne [DecidableEq α] (hl : l₁ <+ l₂) (hl₁ : l₁.IsChain (· ≠ ·)) :
l₁.length ≤ (l₂.destutter (· ≠ ·)).length :=
hl₁.length_le_length_destutter hl
