English
For any ns, if the length of l is at least the sum of the blocks, then the sequence of block lengths of l.splitWrtCompositionAux ns is exactly ns.
Русский
Для любого ns, если длина l не меньше суммы блоков, то последовательность длин блоков l.splitWrtCompositionAux ns равна ns.
LaTeX
$$$\operatorname{map}\,\operatorname{length}(l.splitWrtCompositionAux(ns)) = ns$$$
Lean4
theorem map_length_splitWrtCompositionAux {ns : List ℕ} :
∀ {l : List α}, ns.sum ≤ l.length → map length (l.splitWrtCompositionAux ns) = ns := by
induction ns with
| nil => simp [splitWrtCompositionAux]
| cons n ns IH => grind [splitWrtCompositionAux_cons]