X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ 0 < s.length + 1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ toList s ≠ []
rw [← List.length_pos_iff_ne_nil, length_toList]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ 0 < s.length + 1
exact Nat.succ_pos _