apply Nat.add_lt_add_of_lt
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
⊢ Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
case a
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
⊢ Nat.succ 0 < Nat.succ (Nat.succ (length xs))