norm_cast
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑b
i₁ i₂ : ℕ
hSle : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : i₁ + i₂ ≤ 2 * δ
hi₂ : δ < i₂
⊢ ↑(2 * δ - (i₁ + i₂)) = 2 * ↑δ - (↑i₁ + ↑i₂)
no goals