rw [List.length_append, ih₁, ih₂]
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length (prod [x] (y :: ys) ++ prod (x' :: xs) (y :: ys)) = length (x :: x' :: xs) * length (y :: ys)
α : Type u_1
β : Type u_2
x x' : α
xs : List α
y : β
ys : List β
h_term₁ : Nat.succ 0 + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
h_term₂ : Nat.succ (length xs) + Nat.succ (length ys) < Nat.succ (Nat.succ (length xs)) + Nat.succ (length ys)
ih₁ : length (prod [x] (y :: ys)) = length [x] * length (y :: ys)
ih₂ : length (prod (x' :: xs) (y :: ys)) = length (x' :: xs) * length (y :: ys)
⊢ length [x] * length (y :: ys) + length (x' :: xs) * length (y :: ys) = length (x :: x' :: xs) * length (y :: ys)