simp only [pair, trunc_apply]
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ pair (trunc w) a = pair w a
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
h : ∀ (j : Fin (Nat.succ n)), E w < w j → a j ≤ 0
⊢ ∑ x : Fin (Nat.succ n), a x * min (w x) (E w) = ∑ j : Fin (Nat.succ n), a j * w j