exact False.elim <| Nat.lt_irrefl _ Hx₁'
case hb.inl.inr
δ a b : ℕ
hcop : Nat.Coprime a b
left✝ : 0 < ↑a
i₁ i₂ : ℕ
hi₀ : i₁ + i₂ ≤ 3 * δ
hi₁ : 2 * δ < i₁ + i₂
hi₂ : i₂ ≤ δ
x₂ : ℕ
Hx₂ : ↑x₂ = ↑δ - ↑i₂
hx₂ : x₂ ≤ δ
H : x₂ = 0
Hx₁ : ↑0 = ↑i₁ + ↑i₂ - 2 * ↑δ
Hx₁' : 0 < 0
hx₁ : 0 ≤ δ
ha : a ≤ 0
⊢ b ≤ x₂
no goals