Theorem: ListN.add_elemwise (SciLean/Data/ListN.lean)

State before:
α : Type u_1
n : Nat
inst✝ : Add α
x y : α
xs ys : ListN α n
⊢ cons x xs + cons y ys = cons (x + y) (xs + ys)
Tactic:
rfl
State after:
no goals