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

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