simp only [lec_iff, trunc_apply]
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ trunc w ≤ trunc w'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
h : w ≤ w'
⊢ ∀ (j : Fin (Nat.succ n)), min (w j) (E w) ≤ min (w' j) (E w')