simp only [E_w1, ge_iff_le, tsub_le_iff_right, pair_w1]
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ 1 ≤ E w - pair w ↑a + if a = tw n 1 0 then 0 else 1