have h3 : (660 + (i:ℚ)) * (1319 - (i:ℚ)) ≠ 0 := by
  have h5 : (i: ℚ) < 330 := by norm_cast
  nlinarith
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
⊢ (660 + ↑i) * (1319 - ↑i) / ((660 + ↑i) * (1319 - ↑i)) = 1
i : ℕ
hi : i < 330
h1 : ↑(1319 - i) = 1319 - ↑i
h3 : (660 + ↑i) * (1319 - ↑i) ≠ 0
⊢ (660 + ↑i) * (1319 - ↑i) / ((660 + ↑i) * (1319 - ↑i)) = 1