simp only [E, add_le_add_iff_right]
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ E w ≤ E w'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ Weight.sum w * d / (n + 1) ≤ Weight.sum w' * d / (n + 1)