subst H
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
a b : ℕ
hab : w = of_fraction d a b
s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hi : d < w i
H : of_fraction d s t = w
⊢ False
case intro.intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
a b s t : ℕ
hle : s + t ≤ d
hdom : of_fraction d s t ≤ of_fraction d a b
i : Fin (Nat.succ 2)
hab : of_fraction d s t = of_fraction d a b
hi : d < of_fraction d s t i
⊢ False