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