exact Nat.zero_le _
case neg
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : ∀ (a : ↑(testvecs n d)), 0 ≤ pair' w (v a) → pair' w (v a) ≤ pair' w' (v a)
a : ↑(testvecs n d)
H : pair' w (v a) < 0
⊢ 0 ≤ f w' a
no goals