simp [of_fraction, h.1]
case head
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
h : normalized w
⊢ w { val := 0, isLt := (_ : 0 < Nat.succ 2) } =
    of_fraction d (w 2 - w 1) (w 1) { val := 0, isLt := (_ : 0 < Nat.succ 2) }
no goals