linarith
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hSge : ↑a * (3 * ↑i₂ - ↑(3 * δ)) = ↑b * (2 * ↑(3 * δ) - 3 * ↑i₁ - 3 * ↑i₂)
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₁ : ℕ
Hx₁ : ↑x₁ = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < x₁
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₁ : x₁ ≤ δ
⊢ x₂ ≤ δ
no goals