intro M_LT_N
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
⊢ MultisetLT M N → ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M N : Multiset α
M_LT_N : MultisetLT M N
⊢ ∃ X Y Z, Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y