Theorem: Weight.balanced_iff_lec_E (Weights/Uniqueness.lean)

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
⊢ balanced w ↔ w ≤ ↑(E w)
Tactic:
rfl
State after:
no goals