Theorem: Weight.E_lec_mono (Weights/Weights.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ E w ≤ E w'
Tactic:
simp only [E, add_le_add_iff_right]
State after:
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)

State before:
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)
Tactic:
exact Nat.div_le_div_right (Nat.mul_le_mul_right _ <| sum_le_sum_of_lec w w' h)
State after:
no goals