simpa only [ge_iff_le, tsub_le_iff_right, Nat.sub_add_cancel (h j)] using hw hij
case refine_3
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : Monotone w
h : ∀ (i : Fin (Nat.succ n)), w 0 ≤ w i
i j : Fin (Nat.succ n)
hij : i ≤ j
⊢ (fun i => w i - w 0) i ≤ (fun i => w i - w 0) j
no goals