intro a
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)), f w a ≤ f w' a
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)
⊢ f w a ≤ f w' a