rw [Nat.add_comm]
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) = length xs + 1 + length ys
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)
⊢ length (mergeWith cmp (ys, x :: xs)) = length ys + (length xs + 1)