simp only [mul_zero, tsub_zero, add_zero]
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - (1 - 1) * 0 - 0 + 0
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w