simpa only [ge_iff_le, mul_zero, nonpos_iff_eq_zero, tsub_zero] using h
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : w 0 = 0
hw' : w' 0 = 0
h : E w - (d - 1) * 0 - 0 ≤ E w' - (d - 1) * 0 - 0
⊢ E w ≤ E w'
no goals