simp_rw [f, ← hE]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
a : ↑(testvecs n d)
⊢ f w a ≤ f (trunc w) a
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
a : ↑(testvecs n d)
⊢ E (trunc w) - pair w ↑a ≤ E (trunc w) - pair (trunc w) ↑a