rw [Finset.sum_eq_add_sum_diff_singleton (Finset.mem_univ k)]
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ ∑ j : Fin (Nat.succ n), a j * w j
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ a k * w k + ∑ x in Finset.univ \ {k}, a x * w x