English
Drop a prefix from a Dyck word while preserving the Dyck word structure under a prefix-balance condition.
Русский
Удалить префикс Dyck слова, сохранив структуру слова при условии баланса символов в префиксе.
LaTeX
$$$$ \text{drop}(i, hi) : \text{DyckWord} $$$$
Lean4
/-- Suffix of a Dyck word as a Dyck word, given that the count of `U`s and `D`s in the prefix
are equal. -/
def drop (i : ℕ) (hi : (p.toList.take i).count U = (p.toList.take i).count D) : DyckWord
where
toList := p.toList.drop i
count_U_eq_count_D := by
have := p.count_U_eq_count_D
rw [← take_append_drop i p.toList, count_append, count_append] at this
omega
count_D_le_count_U
k := by
rw [show i = min i (i + k) by omega, ← take_take] at hi
rw [take_drop, ← add_le_add_iff_left (((p.toList.take (i + k)).take i).count U), ← count_append, hi, ← count_append,
take_append_drop]
exact p.count_D_le_count_U _
