constructor
case h.left
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1 ∨ x' ∈ X2 - Y1
case h.left.h
α : Type u_1
pre : Preorder α
dec : DecidableEq α
M N P Y1 X1 Z1 : Multiset α
X1_ne : X1 ≠ ∅
N1_def : N = Z1 + Y1
M1_def : M = Z1 + X1
Ord1 : ∀ x ∈ Y1, ∃ y ∈ X1, x < y
Y2 X2 Z2 : Multiset α
a✝ : X2 ≠ ∅
P2_def : P = Z2 + Y2
N2_def : N = Z2 + X2
Ord2 : ∀ x ∈ Y2, ∃ y ∈ X2, x < y
y : α
y_in_union : y ∈ Y2 + (Y1 - X2)
y_in : y ∈ Y2
x : α
x_in_X2 : x ∈ X2
y_lt_x : y < x
x_in : x ∈ Y1
x' : α
x'_in_X1 : x' ∈ X1
x_lt_x' : x < x'
⊢ x' ∈ X1