cases h with
| RedLt X Y a M nonsense _ =>
  have contra : a ∈ (0 : Multiset α):= by
    rw [nonsense]
    simp_all only [Multiset.mem_add, Multiset.mem_singleton, or_true]
  contradiction
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : LT α
M : Multiset α
h : MultisetRedLt M 0
⊢ False
no goals