. rw [H1]
  have : X = (M - {a0} + {a}) := by
    simp [mul_cons_trivial] at *
    ext b
    rw [Multiset.count_cons]
    simp [Multiset.ext, Multiset.count_cons] at H0
    if h : b = a then
      rw [h]
      have := H0 b
      aesop
    else
      have := H0 b
      simp [mul_erase_trivial]
      aesop
  subst this
  rw [add_comm,mul_cons_trivial]
  aesop
case h.left
α : Type u
inst✝¹ : DecidableEq α
inst✝ : LT α
a : α
M N X Y : Multiset α
a0 : α
H1 : N = X + Y
H0 : a ::ₘ M = X + {a0}
H2 : ∀ y ∈ Y, y < a0
hyp : ¬a = a0
⊢ N = a ::ₘ (Y + (M - {a0}))

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