push_neg at hb
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hb : ¬∀ (j : Fin (Nat.succ n)), w j ≤ E w
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hE : E (trunc w) = E w
k : Fin (Nat.succ n)
hk : w k = 0
w' : Weight n d := Function.update (trunc w) k 1
hb : ∃ j, E w < w j
⊢ E w' = E (trunc w) ∧ balanced w' ∧ trunc w ≤ w' ∧ trunc w ≠ w'