n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sum (take (i + 1) c.blocks) = sum (take i c.blocks) + nthLe c.blocks i h
n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sizeUpTo c (i + 1) = sizeUpTo c i + nthLe c.blocks i h
simp only [sizeUpTo]
no goals
n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sum (take (i + 1) c.blocks) = sum (take i c.blocks) + nthLe c.blocks i h
rw [sum_take_succ _ _ h]