n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sizeUpTo c i < sizeUpTo c i + nthLe c.blocks i h
n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sizeUpTo c i < sizeUpTo c (i + 1)
rw [c.sizeUpTo_succ h]
no goals
n : ℕ
c : Composition n
i : ℕ
h : i < length c
⊢ sizeUpTo c i < sizeUpTo c i + nthLe c.blocks i h
simp