norm_num at hi ⊢
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
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)
hi : 0 ≤ ↑I.a₁ * (↑d - (2 + 1) * ↑(↑i 2)) + ↑I.b₁ * (↑d - (2 + 1) * ↑(↑i 1) + (↑d - (2 + 1) * ↑(↑i 2)))
⊢ 0 ≤ ↑I.a₂ * (↑d - (2 + 1) * ↑(↑i 2)) + ↑I.b₂ * (↑d - (2 + 1) * ↑(↑i 1) + (↑d - (2 + 1) * ↑(↑i 2)))
case hi'
d : ℕ
inst✝ : NeZero d
a b : ℕ
I : BasicInterval
hm : BasicInterval.mem_interior a b I
h : ∀ (a' b' : ℕ), mem_S_le d ↑a' ↑b' → mem a' b' I → a' * I.b₂ = b' * I.a₂
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)
hi : 0 ≤ ↑I.a₁ * (↑d - 3 * ↑(↑i 2)) + ↑I.b₁ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2)))
⊢ 0 ≤ ↑I.a₂ * (↑d - 3 * ↑(↑i 2)) + ↑I.b₂ * (↑d - 3 * ↑(↑i 1) + (↑d - 3 * ↑(↑i 2)))