exact Nat.mul_div_le_mul_div_assoc ..
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
⊢ Nat.succ k * (Weight.sum w * d / (n + 1)) ≤ Nat.succ k * (Weight.sum w * d) / (n + 1)
no goals