English
Under a suitable equivalence condition, moving the head element from b to a in front of a list preserves a length-order constraint for destutter'.
Русский
При подходящем условии эквивалентности перемещение головного элемента списка сохраняет порядок длин destutter'.
LaTeX
$$$\\forall l,\\ (l.destutter'_R b).length \\le ((b \\!:\\! l).destutter'_R a).length$$$
Lean4
/-- `List.destutter'` on a relation like ≠, whose negation is an equivalence, has length
monotonic under List.cons -/
/-
TODO: Replace this lemma by the more general version:
theorem Sublist.length_destutter'_mono [IsEquiv α Rᶜ] (h : a :: l₁ <+ b :: l₂) :
(List.destutter' R a l₁).length ≤ (List.destutter' R b l₂).length
-/
theorem le_length_destutter'_cons [IsEquiv α Rᶜ] :
∀ {l : List α}, (l.destutter' R b).length ≤ ((b :: l).destutter' R a).length
| [] => by by_cases hab : (R a b) <;> simp_all [Nat.le_succ]
| c :: cs => by
by_cases hab : R a b
case pos => simp [destutter', if_pos hab, Nat.le_succ]
obtain hac | hac : R a c ∨ Rᶜ a c := em _
· have hbc : ¬Rᶜ b c := mt (_root_.trans hab) (not_not.2 hac)
simp [destutter', if_pos hac, if_pos (not_not.1 hbc), if_neg hab]
· have hbc : ¬R b c := trans (symm hab) hac
simp only [destutter', if_neg hbc, if_neg hac, if_neg hab]
exact (length_destutter'_congr cs hab).ge
