contrapose! hw
case intro.intro.intro.intro.intro
d : ℕ
inst✝ : NeZero d
w : Weight 2 d
hw : w ∈ M 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)), w i ≤ d
case 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
hw : ∃ i, d < w i
⊢ w ∉ M 2 d