English
If p.toList is a suffix of q.toList, then p ≤ q in the DyckWord order.
Русский
Если p.toList является суффиксом q.toList, то p ≤ q в порядке DyckWord.
LaTeX
$$$ p^{\text{toList}} \text{ isSuffix of } q^{\text{toList}} \Rightarrow p \le q $$$
Lean4
theorem le_of_suffix (h : p.toList <:+ q.toList) : p ≤ q :=
by
obtain ⟨r', h⟩ := h
have hc :
(q.toList.take (q.toList.length - p.toList.length)).count U =
(q.toList.take (q.toList.length - p.toList.length)).count D :=
by
have hq := q.count_U_eq_count_D
rw [← h] at hq ⊢
rw [count_append, count_append, p.count_U_eq_count_D, Nat.add_right_cancel_iff] at hq
simp [hq]
let r : DyckWord := q.take _ hc
have e : r' = r := by simp_rw [r, take, ← h, length_append, add_tsub_cancel_right, take_left']
rw [e] at h; replace h : r + p = q := DyckWord.ext h; rw [← h]; exact le_add_self ..
