refine (Nat.sub_le_sub_right (E_trunc_le_E w) _).trans ?_
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
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a