English
In the prefix up to firstReturn + 1, the counts of U and D are equal.
Русский
В префиксе до firstReturn + 1 количества U и D равны.
LaTeX
$$$$ (p.toList.take(p.firstReturn+1)).count U = (p.toList.take(p.firstReturn+1)).count D. $$$$
Lean4
/-- The left part of the Dyck word decomposition,
inside the `U, D` pair that `firstReturn` refers to. `insidePart 0 = 0`. -/
def insidePart : DyckWord :=
if h : p = 0 then 0
else
(p.take (p.firstReturn + 1) (count_take_firstReturn_add_one h)).denest
⟨by rw [← toList_ne_nil, take]; simpa using toList_ne_nil.mpr h, fun i lb ub ↦
by
simp only [take, length_take, lt_min_iff] at ub ⊢
replace ub := ub.1
rw [take_take, min_eq_left ub.le]
rw [show i = i - 1 + 1 by cutsat] at ub ⊢
rw [Nat.add_lt_add_iff_right] at ub
exact count_D_lt_count_U_of_lt_firstReturn ub⟩
