zify at h
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
bb : ℕ
hbb : ↑bb = bi
H : ¬0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hmem : mem aa bb I
h : aa * I.b₁ = bb * I.a₁
⊢ False
case hi'.inr.intro.intro
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
k₁ k₂ : ℕ
hk₁ : 0 < k₁
hk₂ : 0 < k₂
h₁ : a = k₁ * I.a₁ + k₂ * I.a₂
h₂ : b = k₁ * I.b₁ + k₂ * I.b₂
i : ↑(testvecs 2 d)
bi : ℤ := ↑d - 3 * ↑(↑i 2)
hbi_def : bi = ↑d - 3 * ↑(↑i 2)
ai : ℤ := ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hi : 0 ≤ ↑I.a₂ * bi + ↑I.b₂ * ai
hai_def : ai = ↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2))
hai : ai < 0
hbi : 0 ≤ bi
memS : mem_S_ge d (-ai) bi
aa : ℕ
haa : ↑aa = -ai
bb : ℕ
hbb : ↑bb = bi
H : ¬0 ≤ ↑I.a₁ * bi + ↑I.b₁ * ai
hmem : mem aa bb I
h : ↑aa * ↑I.b₁ = ↑bb * ↑I.a₁
⊢ False