aesop
α : 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
y_in : y ∈ Y1 - X2
h : y ∈ Y1 → ∃ y_1 ∈ X1, y < y_1 := Ord1 y
⊢ Y1 - X2 ≤ Y1
no goals