induction Y using Multiset.strongInductionOn
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
Y : Multiset α
Y_not_empty : Y ≠ ∅
⊢ ∀ (M N X Z : Multiset α), M = Z + X → N = Z + Y → (∀ x ∈ X, ∃ y ∈ Y, x < y) → TC MultisetRedLt M N
case ih
α : Type u_1
dec : DecidableEq α
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x y => x < y
s✝ : Multiset α
a✝ :
  ∀ t < s✝, t ≠ ∅ → ∀ (M N X Z : Multiset α), M = Z + X → N = Z + t → (∀ x ∈ X, ∃ y ∈ t, x < y) → TC MultisetRedLt M N
Y_not_empty : s✝ ≠ ∅
⊢ ∀ (M N X Z : Multiset α), M = Z + X → N = Z + s✝ → (∀ x ∈ X, ∃ y ∈ s✝, x < y) → TC MultisetRedLt M N