cases' eq_or_ne i j with h h
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
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a
case inl
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
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a

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
⊢ pair w (Weight.comp a (Equiv.swap i j)) ≤ pair w a