rw [← tsub_add_eq_add_tsub hle, ← tsub_add_eq_add_tsub (mul_le_mul' le_rfl hle),
    ← Nat.mul_sub_left_distrib]
case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
case H.inr
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
a : Weight n d
h✝ : a ∈ testvecs n d
m : ℕ := Weight.sum w * d / (n + 1)
l : ℕ := pair w a
hle : l ≤ m
⊢ m - l + 1 ≤ Nat.succ k * (m - l) + 1