refine Int.le_add_one (Int.le_ediv_of_mul_le (by linarith) ?_)
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) ≤ ↑(Weight.sum w) * ↑d / (↑n + 1) + 1
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(pair w ↑a) * (↑n + 1) ≤ ↑(Weight.sum w) * ↑d