unfold MultisetLt
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
M N X Y Z : Multiset α
Y_not_empty : Y ≠ ∅
MZX : M = Z + X
NZY : N = Z + Y
h : ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ MultisetLt M N
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
M N X Y Z : Multiset α
Y_not_empty : Y ≠ ∅
MZX : M = Z + X
NZY : N = Z + Y
h : ∀ x ∈ X, ∃ y ∈ Y, x < y
⊢ TC MultisetRedLt M N