simp only [pair'_v, sub_neg] at h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : pair' w (v a) < 0
⊢ f w a = 0
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ↑d * ↑(Weight.sum w) < (↑n + 1) * ↑(pair w ↑a)
⊢ f w a = 0