case h
n : ℕ
c : Composition n
h : 0 < n
⊢ 0 < sum c.blocks
n : ℕ
c : Composition n
h : 0 < n
⊢ 0 < length c
apply length_pos_of_sum_pos
case h.e'_4
n : ℕ
c : Composition n
h : 0 < n
⊢ sum c.blocks = n
case h
n : ℕ
c : Composition n
h : 0 < n
⊢ 0 < sum c.blocks
convert h
no goals
case h.e'_4
n : ℕ
c : Composition n
h : 0 < n
⊢ sum c.blocks = n
exact c.blocks_sum