exact (Nat.le_mul_of_pos_left _ ha).trans hm
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 * E w ≤ pair (trunc w) a
⊢ E w ≤ pair (trunc w) a
no goals