rw [Nat.sub_eq_zero_of_le (trunc_pair_lb w a h)]
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∃ j, E w < w j ∧ 0 < ↑a j
⊢ 0 ≤ E w - pair w ↑a