exact Nat.sub_le_sub_left (trunc_pair_le_pair 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
no goals