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

State before:
n d : ℕ
inst✝ : NeZero d
w : Weight n d
j : Fin (Nat.succ n)
⊢ trunc w j ≤ E w
Tactic:
simp only [trunc, min_le_iff, le_refl, or_true]
State after:
no goals