simp only [pair'_v, sub_nonneg] at h
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : 0 ≤ pair' w (v a)
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1