exact add_le_add_right (Nat.le_mul_of_pos_left _ (Nat.succ_pos k)) 1
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
no goals