exact mul_add_mul_le_mul_add_mul ha hw
case inr
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
i j : Fin (Nat.succ n)
hw : w i ≤ w j
ha : a i ≤ a j
h : i ≠ j
haij : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k = a k
ht : ∀ {k : Fin (Nat.succ n)}, k ∈ erase (erase univ j) i → Weight.comp a (Equiv.swap i j) k * w k = a k * w k
⊢ a i * w j + a j * w i ≤ a i * w i + a j * w j
no goals