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