induction M using Multiset.induction_on with | empty =>
  constructor
  intro y y_lt
  absurd y_lt
  apply not_MultisetRedLt_0
| cons _ _ ih =>
  apply mord_wf_3
  . assumption
  . apply wf_el
    simp_all
  . apply ih
    intros
    apply wf_el
    simp_all
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Preorder α
M : Multiset α
wf_el : ∀ x ∈ M, Acc LT.lt x
⊢ AccM_1 M
no goals