cases' lt_or_le m l with hlt hle
case H
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
⊢ m + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l
case H.inl
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
hlt : m < l
⊢ 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 + 1 - l ≤ Nat.succ k * m + 1 - Nat.succ k * l