rcases LTNM with ⟨Y1, X1, Z1, X1_ne, N1_def, M1_def, Ord1⟩
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
LTNM : MultisetLT N M
LTPN : MultisetLT P N
⊢ MultisetLT P M
case MLT
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P : Multiset α
LTPN : MultisetLT P N
Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
⊢ MultisetLT P M