exact (le_of_le_of_eq (hw.2 (le_of_le_of_eq hij hj)) hm).trans zero_le_one
case pos
n d : ℕ
inst✝ : NeZero d
w : Weight n d
hw : normalized w
P : ℕ → Prop := fun i => if hi : i < Nat.succ n then w { val := i, isLt := hi } = 0 else False
hP : ∀ (m : ℕ) (hm : m < Nat.succ n), P m ↔ w { val := m, isLt := hm } = 0
m : Fin (Nat.succ n) := { val := Nat.findGreatest P n, isLt := (_ : Nat.findGreatest P n < Nat.succ n) }
hm : w m = 0
i j : Fin (Nat.succ n)
hij : i ≤ j
hi : ¬i = m
hj : j = m
⊢ w i ≤ 1
no goals