simp only [trunc_apply, min_le_iff, le_min_iff, le_refl, and_true, or_true]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ trunc w i ≤ trunc w j
n d : ℕ
inst✝ : NeZero d
w : Weight n d
h : Monotone w
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ w i ≤ w j ∨ E w ≤ w j