by_contra hb
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
⊢ balanced w
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
hmin : ∀ (u : Weight n d), Monotone u → u ≤ w → w ≤ u
hb : ¬balanced w
⊢ False