simp [pair]
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
k : Fin (Nat.succ n)
⊢ a k * w k ≤ pair w a
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