n : ℕ
c : Composition n
⊢ length c ≤ sum c.blocks
n : ℕ
c : Composition n
⊢ length c ≤ n
conv_rhs => rw [← c.blocks_sum]
no goals
n : ℕ
c : Composition n
⊢ length c ≤ sum c.blocks
exact length_le_sum_of_one_le _ fun i hi => c.one_le_blocks hi