case h.intro.inr h =>
  rcases h with ⟨H, H0⟩
  rw [H]
  clear H induction x using Multiset.induction with
  | empty =>
    simpa
  | cons h =>
    simp_all only [Multiset.mem_cons, or_true, implies_true, true_implies, forall_eq_or_imp, Multiset.add_cons]
α : Type u
x✝ : Multiset α
inst✝¹ : DecidableEq α
inst✝ : Preorder α
a : α
M0 : Multiset α
H1 : ∀ (b : α) (M : Multiset α), b < a → AccM_1 M → AccM_1 (b ::ₘ M)
H2 : AccM_1 M0
H3 : ∀ (M : Multiset α), MultisetRedLt M M0 → AccM_1 (a ::ₘ M)
N : Multiset α
N_lt : MultisetRedLt N (a ::ₘ M0)
x : Multiset α
h : N = M0 + x ∧ ∀ x_1 ∈ x, x_1 < a
⊢ AccM_1 N
no goals