case e_a.e_a
n : ℕ
α : Type u_1
l : List α
c : Composition (length l)
i : ℕ
⊢ map length (splitWrtComposition l c) = c.blocks
n : ℕ
α : Type u_1
l : List α
c : Composition (length l)
i : ℕ
⊢ sum (take i (map length (splitWrtComposition l c))) = Composition.sizeUpTo c i
congr
no goals
case e_a.e_a
n : ℕ
α : Type u_1
l : List α
c : Composition (length l)
i : ℕ
⊢ map length (splitWrtComposition l c) = c.blocks
exact map_length_splitWrtComposition l c