X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
⊢ s₂.length = 0 → s₁.length = 0
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
⊢ ¬0 < s₂.length → ¬0 < s₁.length
simp only [pos_iff_ne_zero, Ne.def, not_iff_not, Classical.not_not]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : bot s₁ = bot s₂
ht : top s₁ = top s₂
⊢ s₂.length = 0 → s₁.length = 0
exact length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero hb.symm ht.symm