have hm := sorted_is_Monotone w
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
⊢ normalized (sorted w)
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
⊢ normalized (sorted w)