English
If Rᶜ is an equivalence relation and ¬R a b, then the lengths of destutter' with respect to R are equal when starting from a or b.
Русский
Если комплемент отношения Rᶜ является эквивалентностью и ¬R a b, то длины destutter' по отношению к R одинаковы при начале с a или с b.
LaTeX
$$$\\text{len}(\\mathrm{destutter}'_R(a,l)) = \\text{len}(\\mathrm{destutter}'_R(b,l)) \\quad\\text{если } \\neg R(a,b) \\text{ и } IsEquiv(\\alpha, R^c).$$$
Lean4
/-- `List.destutter'` on a relation like `≠`, whose negation is an equivalence, gives the same
length if the first elements are not related. -/
theorem length_destutter'_congr [IsEquiv α Rᶜ] (hab : ¬R a b) : (l.destutter' R a).length = (l.destutter' R b).length :=
(length_destutter'_cotrans_ge hab).antisymm <| length_destutter'_cotrans_ge (symm hab : Rᶜ b a)
