theorem congr_args {x₀ : ℤ} {y₀ : ℤ} {a : ℤ} {b : ℤ} {x : ℤ} {y : ℤ} : (x, y) = (x₀, y₀) → a * x + b * y = a * x₀ + b * y₀

theorem lemma_1_64 (x₀ : ℤ) (y₀ : ℤ) (a : ℤ) (b : ℤ) (x : ℤ) (y : ℤ) (h1 : a > 0) (h2 : b > 0) (h5 : IsCoprime a b) (h6 : x₀ < b) (h7 : y₀ < a) (h8 : x ≥ 0) (h9 : y ≥ 0) : a * x + b * y = a * x₀ + b * y₀ ↔ (x, y) = (x₀, y₀)