rw [add_comm,mul_cons_trivial]
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N Y : Multiset α
a0 : α
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H1 : N = M - {a0} + {a} + Y
H0 : a ::ₘ M = M - {a0} + {a} + {a0}
⊢ M - {a0} + {a} + Y = a ::ₘ (Y + (M - {a0}))
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N Y : Multiset α
a0 : α
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
H1 : N = M - {a0} + {a} + Y
H0 : a ::ₘ M = M - {a0} + {a} + {a0}
⊢ Y + a ::ₘ (M - {a0}) = a ::ₘ (Y + (M - {a0}))