cases LTMN
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
M N : Multiset α
LTMN : MultisetLT M N
⊢ MultisetLt M N
case MLT
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
M N X✝ Y✝ Z✝ : Multiset α
a✝³ : Y✝ ≠ ∅
a✝² : M = Z✝ + X✝
a✝¹ : N = Z✝ + Y✝
a✝ : ∀ x ∈ X✝, ∃ y ∈ Y✝, x < y
⊢ MultisetLt M N