have hm := mul_le_pair w.trunc a j
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
⊢ E w ≤ pair (trunc w) a
case intro.intro
n d : ℕ
inst✝ : NeZero d
w a : Weight n d
j : Fin (Nat.succ n)
hj : E w < w j
ha : 0 < a j
hm : a j * trunc w j ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a