English
If the negation of a relation R is transitive, then changing the first element of a list from a to b with ¬R a b does not increase the length of the destutter' of the list.
Русский
Если отрицание отношения R переносимо по транзитивности, то замена первого элемента списка a на b с условием ¬R a b не увеличивает длину destutter' списка.
LaTeX
$$$\\text{len}(\\mathrm{destutter}'_R(b,l)) \\le \\text{len}(\\mathrm{destutter}'_R(a,l)) \\quad\\text{whenever } \\neg R(a,b) \\text{ and } IsTrans^{-1}(R^c).$$$
Lean4
/-- `destutter'` on a relation like ≠ or <, whose negation is transitive, has length monotone
under a `¬R` changing of the first element. -/
theorem length_destutter'_cotrans_ge [i : IsTrans α Rᶜ] :
∀ {a} {l : List α}, ¬R b a → (l.destutter' R b).length ≤ (l.destutter' R a).length
| a, [], hba => by simp
| a, c :: l, hba => by
by_cases hbc : R b c
case pos =>
have hac : ¬Rᶜ a c := (mt (_root_.trans hba)) (not_not.2 hbc)
simp_rw [destutter', if_pos (not_not.1 hac), if_pos hbc, length_cons, le_refl]
case neg =>
simp only [destutter', if_neg hbc]
by_cases hac : R a c
case pos =>
simp only [if_pos hac, length_cons]
exact Nat.le_succ_of_le (length_destutter'_cotrans_ge hbc)
case neg =>
simp only [if_neg hac]
exact length_destutter'_cotrans_ge hba
