specialize h (tw n d 0)
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : ∀ (a : ↑(testvecs n d)), f w a ≤ f w' a
⊢ E w ≤ E w'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : f w (tw n d 0) ≤ f w' (tw n d 0)
⊢ E w ≤ E w'