refine not_in_M_of_dom_ne ⟨of_fraction d s t, normalized_of_of_fraction d s t, hab ▸ hdom,
                           fun 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
⊢ w ∉ M 2 d
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