have H : w.sum * d / (n + 1) + 1 - w.pair a
           ≤ k.succ * (w.sum * d / (n + 1)) + 1 - k.succ * w.pair a
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a
case H
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a

n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
H : Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * (Weight.sum w * d / (n + 1)) + 1 - Nat.succ k * pair w a
⊢ Weight.sum w * d / (n + 1) + 1 - pair w a ≤ Nat.succ k * Weight.sum w * d / (n + 1) + 1 - Nat.succ k * pair w a