exact ⟨Nat.eq_zero_of_le_zero (le_of_le_of_eq (hm (Fin.zero_le _)) h₁), sorted_is_Monotone w⟩
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : w 0 = 0
hm : Monotone (sorted w)
h₁ : sorted w ((Tuple.sort w)⁻¹ 0) = 0
⊢ normalized (sorted w)
no goals