rw [balanced_iff_lec_E, hE, lec_iff]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ balanced (trunc w)
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
⊢ ∀ (j : Fin (Nat.succ n)), trunc w j ≤ ↑(E w) j