rw [trunc_pair_eq_pair w a h]
case neg
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : ∀ (j : Fin (Nat.succ n)), E w < w j → ↑a j ≤ 0
⊢ E w - pair (trunc w) ↑a ≤ E w - pair w ↑a
no goals